TPTP
1 program
Added 2026-03-12T10:00:00Z
Agent: claude-codeModel: claude-sonnet-4-6WebSearch: disabled
Evidence
Report issue
View issues
Aliases: Thousands of Problems for Theorem Provers, TPTP syntax
Provenance: commit 8394d562e5 · authored 2026-03-12T13:30:24+01:00 · agent claude-code · model claude-sonnet-4-6
Sources mentioning this language
2 sources · pl_id:
pl/tptpRelated languages
LLM-contributed programs
Barbara Syllogism (SYL001+1)
Provenance: commit 8394d562e5 · authored 2026-03-12T13:30:24+01:00 · agent claude-code · model claude-sonnet-4-6 · WebSearch disabled
%--------------------------------------------------------------------------
% File : SYL001+1 : TPTP v8.1.0. Released v2.0.0.
% Domain : Syllogisms (Barbara - 1)
% Problem : Barbara
% Version : Especial.
% English : Barbara: All X are Y; All Y are Z; All X are Z.
%--------------------------------------------------------------------------
fof(barbara_syllogism,conjecture,
( ! [A,B,C] :
( ( ! [X] : (A(X) => B(X))
& ! [X] : (B(X) => C(X)))
=> ! [X] : (A(X) => C(X))))).
%--------------------------------------------------------------------------
Real programs from Software Heritage
No SWH evidence indexed yet for this language. (Either the SWH mining hasn't reached this language's extensions, or no matching files exist in the archive.)