%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : BOO109+1 : TPTP v9.2.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:11:27 PM UTC 2026
% Result : Theorem 232.40s 150.58s
% Output : CNFRefutation 232.60s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_72)
% Comments :
%------------------------------------------------------------------------------
fof(tautology,conjecture,
! [X1,X2] : p(nand(nand(X1,nand(X2,X2)),nand(nand(nand(X2,X2),nand(nand(X1,X1),nand(X1,X1))),nand(nand(X2,X2),nand(nand(X1,X1),nand(X1,X1)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tautology) ).
fof(wajsbergs_axiom,axiom,
! [X1,X2,X3,X4] : p(nand(nand(X1,nand(X2,X3)),nand(nand(nand(X4,X3),nand(nand(X1,X4),nand(X1,X4))),nand(X1,nand(X1,X2))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wajsbergs_axiom) ).
fof(modus_ponens_for_nand,axiom,
! [X5,X6,X7] :
( ( p(nand(X5,nand(X6,X7)))
& p(X5) )
=> p(X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',modus_ponens_for_nand) ).
fof(i_0_3,negated_conjecture,
~ ! [X1,X2] : p(nand(nand(X1,nand(X2,X2)),nand(nand(nand(X2,X2),nand(nand(X1,X1),nand(X1,X1))),nand(nand(X2,X2),nand(nand(X1,X1),nand(X1,X1)))))),
inference(assume_negation,[status(cth)],[tautology]) ).
fof(i_0_4,negated_conjecture,
~ p(nand(nand(esk1_0,nand(esk2_0,esk2_0)),nand(nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0))),nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0)))))),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_3])])]) ).
fof(i_0_5,plain,
! [X17,X18,X19,X20] : p(nand(nand(X17,nand(X18,X19)),nand(nand(nand(X20,X19),nand(nand(X17,X20),nand(X17,X20))),nand(X17,nand(X17,X18))))),
inference(variable_rename,[status(thm)],[wajsbergs_axiom]) ).
fof(i_0_6,plain,
! [X21,X22,X23] :
( ~ p(nand(X21,nand(X22,X23)))
| ~ p(X21)
| p(X23) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[modus_ponens_for_nand])]) ).
cnf(i_0_7,negated_conjecture,
~ p(nand(nand(esk1_0,nand(esk2_0,esk2_0)),nand(nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0))),nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0)))))),
inference(split_conjunct,[status(thm)],[i_0_4]),
[final] ).
cnf(i_0_8,plain,
p(nand(nand(X1,nand(X2,X3)),nand(nand(nand(X4,X3),nand(nand(X1,X4),nand(X1,X4))),nand(X1,nand(X1,X2))))),
inference(split_conjunct,[status(thm)],[i_0_5]),
[final] ).
cnf(i_0_9,plain,
( p(X3)
| ~ p(nand(X1,nand(X2,X3)))
| ~ p(X1) ),
inference(split_conjunct,[status(thm)],[i_0_6]),
[final] ).
cnf(i_0_75,plain,
p(nand(nand(nand(X1,X2),nand(nand(nand(X2,nand(X3,X4)),nand(X2,nand(X3,X4))),X1)),nand(X1,X2))),
inference(scs_inference,[],[i_0_72,i_0_20,i_0_9]) ).
cnf(c_0_80,plain,
( p(X1)
| ~ p(nand(X2,nand(X3,X1)))
| ~ p(X2) ),
i_0_9 ).
cnf(c_0_81,plain,
p(nand(nand(X1,nand(X2,X3)),nand(nand(nand(X4,X3),nand(nand(X1,X4),nand(X1,X4))),nand(X1,nand(X1,X2))))),
i_0_8 ).
cnf(c_0_82,plain,
( p(nand(X1,nand(X1,X2)))
| ~ p(nand(X1,nand(X2,X3))) ),
inference(spm,[status(thm)],[c_0_80,c_0_81]) ).
cnf(c_0_83,plain,
( p(X1)
| ~ p(nand(X2,nand(X1,X3)))
| ~ p(X2) ),
inference(spm,[status(thm)],[c_0_80,c_0_82]) ).
cnf(c_0_84,plain,
( p(nand(nand(X1,X2),nand(nand(X3,X1),nand(X3,X1))))
| ~ p(nand(X3,nand(X4,X2))) ),
inference(spm,[status(thm)],[c_0_83,c_0_81]) ).
cnf(c_0_85,negated_conjecture,
~ p(nand(nand(esk1_0,nand(esk2_0,esk2_0)),nand(nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0))),nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0)))))),
i_0_7 ).
cnf(c_0_86,plain,
( p(nand(X1,X2))
| ~ p(nand(X1,nand(X3,X4)))
| ~ p(nand(X2,X4)) ),
inference(spm,[status(thm)],[c_0_80,c_0_84]) ).
cnf(c_0_87,negated_conjecture,
( ~ p(nand(nand(nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0))),nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0)))),X1))
| ~ p(nand(nand(esk1_0,nand(esk2_0,esk2_0)),nand(X2,X1))) ),
inference(spm,[status(thm)],[c_0_85,c_0_86]) ).
cnf(c_0_88,plain,
( ~ p(nand(nand(nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0))),nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0)))),nand(X1,esk1_0)))
| ~ p(nand(X1,nand(X2,nand(esk2_0,esk2_0)))) ),
inference(spm,[status(thm)],[c_0_87,c_0_84]) ).
cnf(c_0_89,plain,
( p(nand(X1,nand(X1,X1)))
| ~ p(nand(X1,nand(X2,X3))) ),
inference(spm,[status(thm)],[c_0_82,c_0_82]) ).
cnf(c_0_90,plain,
( ~ p(nand(nand(nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0))),nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0)))),nand(X1,esk1_0)))
| ~ p(nand(X1,nand(nand(esk2_0,esk2_0),X2))) ),
inference(spm,[status(thm)],[c_0_88,c_0_82]) ).
cnf(c_0_91,plain,
( p(nand(nand(X1,X2),nand(nand(X1,X2),nand(X1,X2))))
| ~ p(nand(X3,nand(X4,X2))) ),
inference(spm,[status(thm)],[c_0_89,c_0_84]) ).
cnf(c_0_92,plain,
p(nand(nand(nand(X1,X2),nand(nand(nand(X2,nand(X3,X4)),nand(X2,nand(X3,X4))),X1)),nand(X1,X2))),
i_0_75 ).
cnf(c_0_93,plain,
( ~ p(nand(nand(nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0))),nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0)))),nand(X1,esk1_0)))
| ~ p(nand(nand(nand(esk2_0,esk2_0),X2),X3))
| ~ p(nand(X1,nand(X4,X3))) ),
inference(spm,[status(thm)],[c_0_90,c_0_86]) ).
cnf(c_0_94,plain,
p(nand(nand(X1,X2),nand(nand(X1,X2),nand(X1,X2)))),
inference(spm,[status(thm)],[c_0_91,c_0_92]) ).
cnf(c_0_95,plain,
( ~ p(nand(nand(nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0))),nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0)))),nand(nand(X1,X2),esk1_0)))
| ~ p(nand(nand(nand(esk2_0,esk2_0),X3),nand(X1,X2))) ),
inference(spm,[status(thm)],[c_0_93,c_0_94]) ).
cnf(c_0_96,plain,
( p(nand(X1,nand(X2,X3)))
| ~ p(nand(X1,nand(X4,nand(nand(X2,X3),nand(X2,X3))))) ),
inference(spm,[status(thm)],[c_0_86,c_0_94]) ).
cnf(c_0_97,plain,
~ p(nand(nand(nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0))),nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0)))),nand(nand(nand(nand(esk2_0,esk2_0),X1),nand(nand(esk2_0,esk2_0),X1)),esk1_0))),
inference(spm,[status(thm)],[c_0_95,c_0_94]) ).
cnf(c_0_98,plain,
p(nand(nand(nand(X1,X2),nand(X1,X2)),nand(X1,X2))),
inference(spm,[status(thm)],[c_0_96,c_0_94]) ).
cnf(c_0_99,plain,
~ p(nand(nand(nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0))),nand(nand(esk2_0,esk2_0),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0)))),nand(esk1_0,X1))),
inference(spm,[status(thm)],[c_0_97,c_0_82]) ).
cnf(c_0_100,plain,
( p(nand(nand(nand(X1,X2),nand(X1,X2)),X3))
| ~ p(nand(X3,X2)) ),
inference(spm,[status(thm)],[c_0_86,c_0_98]) ).
cnf(c_0_101,plain,
~ p(nand(nand(esk1_0,X1),nand(nand(esk1_0,esk1_0),nand(esk1_0,esk1_0)))),
inference(spm,[status(thm)],[c_0_99,c_0_100]) ).
cnf(c_0_102,plain,
$false,
inference(spm,[status(thm)],[c_0_101,c_0_94]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : BOO109+1 : TPTP v9.2.1. Released v3.5.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.12/0.31 % Computer : n015.cluster.edu
% 0.12/0.31 % Model : x86_64 x86_64
% 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.31 % Memory : 8042.1875MB
% 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.31 % CPULimit : 300
% 0.12/0.31 % WCLimit : 300
% 0.12/0.31 % DateTime : Tue May 5 10:47:31 EDT 2026
% 0.12/0.32 % CPUTime :
% 0.12/0.33 % start to proof: theBenchmark
% 232.40/150.58 % Version : CSE_E---1.7
% 232.40/150.58 % Problem : theBenchmark.p
% 232.40/150.58 % SZS status Theorem for theBenchmark.p
% 232.40/150.58 % SZS output start CNFRefutation
% See solution above
% 232.60/150.70 % Total time : 150.069s
%------------------------------------------------------------------------------