%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYN719-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n028.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 : Fri Jul 25 09:28:22 PM UTC 2025
% Result : Unsatisfiable 0.18s 0.38s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named p7_3)
% Comments :
%------------------------------------------------------------------------------
cnf(2,plain,
p7(X0,X0),
inference(cnf,[status(esa)],[p7_3]) ).
cnf(l0,plain,
p7(c82,c82),
inference(instantiation,[status(thm)],[2]) ).
cnf(95,plain,
( ~ p7(X0,X1)
| ~ p15(X2,X3)
| ~ p67(X2,X0)
| p67(X3,X1) ),
inference(cnf,[status(esa)],[p67_96]) ).
cnf(l1,plain,
( ~ p7(c82,c82)
| ~ p15(f16(c80,c81),f16(c80,f23(f26(c84,c85),c81)))
| ~ p67(f16(c80,c81),c82)
| p67(f16(c80,f23(f26(c84,c85),c81)),c82) ),
inference(instantiation,[status(thm)],[95]) ).
cnf(88,plain,
( ~ p15(X0,X1)
| ~ p15(X0,X2)
| p15(X1,X2) ),
inference(cnf,[status(esa)],[p15_89]) ).
cnf(l16,plain,
( ~ p15(f16(c80,f23(f26(c84,c85),c81)),f16(c80,c81))
| ~ p15(f16(c80,f23(f26(c84,c85),c81)),f16(c80,f23(f26(c84,c85),c81)))
| p15(f16(c80,c81),f16(c80,f23(f26(c84,c85),c81))) ),
inference(instantiation,[status(thm)],[88]) ).
cnf(122,plain,
( ~ p13(X0,X1)
| ~ p14(X2,X3)
| p15(f16(X0,X2),f16(X1,X3)) ),
inference(cnf,[status(esa)],[p15_123]) ).
cnf(l17,plain,
( ~ p13(c80,c80)
| ~ p14(f23(f26(c84,c85),c81),c81)
| p15(f16(c80,f23(f26(c84,c85),c81)),f16(c80,c81)) ),
inference(instantiation,[status(thm)],[122]) ).
cnf(44,plain,
p14(f23(f26(c84,c85),X0),X0),
inference(cnf,[status(esa)],[p14_45]) ).
cnf(l21,plain,
p14(f23(f26(c84,c85),c81),c81),
inference(instantiation,[status(thm)],[44]) ).
cnf(41,plain,
p67(f16(c80,c81),c82),
inference(cnf,[status(esa)],[p67_42]) ).
cnf(l3,plain,
p67(f16(c80,c81),c82),
inference(instantiation,[status(thm)],[41]) ).
cnf(125,plain,
( ~ p14(X0,f23(f26(c84,X1),X2))
| ~ p66(f12(c78,c77),X3)
| ~ p67(f16(c80,X2),c82)
| ~ p69(f36(c86,f38(X1,f40(f42(f44(f46(c87,X3),X0),X1),X2))),f30(c88,f32(c89,f8(c75,c76))))
| p68(f19(f21(c83,c77),X3),X0) ),
inference(cnf,[status(esa)],[p68_126]) ).
cnf(l18,plain,
( ~ p14(f23(f26(c84,c85),c81),f23(f26(c84,c85),f23(f26(c84,c85),c81)))
| ~ p66(f12(c78,c77),c79)
| ~ p67(f16(c80,f23(f26(c84,c85),c81)),c82)
| ~ p69(f36(c86,f38(c85,f40(f42(f44(f46(c87,c79),f23(f26(c84,c85),c81)),c85),f23(f26(c84,c85),c81)))),f30(c88,f32(c89,f8(c75,c76))))
| p68(f19(f21(c83,c77),c79),f23(f26(c84,c85),c81)) ),
inference(instantiation,[status(thm)],[125]) ).
cnf(38,plain,
p13(X0,X0),
inference(cnf,[status(esa)],[p13_39]) ).
cnf(l25,plain,
p13(c80,c80),
inference(instantiation,[status(thm)],[38]) ).
cnf(40,plain,
p66(f12(c78,c77),c79),
inference(cnf,[status(esa)],[p66_41]) ).
cnf(l19,plain,
p66(f12(c78,c77),c79),
inference(instantiation,[status(thm)],[40]) ).
cnf(36,plain,
p15(X0,X0),
inference(cnf,[status(esa)],[p15_37]) ).
cnf(l27,plain,
p15(f16(c80,f23(f26(c84,c85),c81)),f16(c80,f23(f26(c84,c85),c81))),
inference(instantiation,[status(thm)],[36]) ).
cnf(51,plain,
( ~ p70(X0,X1)
| p69(f36(c86,X1),X0) ),
inference(cnf,[status(esa)],[p69_52]) ).
cnf(l22,plain,
( ~ p70(f30(c88,f32(c89,f8(c75,c76))),f38(c85,f40(f42(f44(f46(c87,c79),f23(f26(c84,c85),c81)),c85),f23(f26(c84,c85),c81))))
| p69(f36(c86,f38(c85,f40(f42(f44(f46(c87,c79),f23(f26(c84,c85),c81)),c85),f23(f26(c84,c85),c81)))),f30(c88,f32(c89,f8(c75,c76)))) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(96,plain,
( ~ p7(X0,X1)
| ~ p14(X2,X3)
| ~ p68(X0,X2)
| p68(X1,X3) ),
inference(cnf,[status(esa)],[p68_97]) ).
cnf(l41,plain,
( ~ p7(f19(f21(c83,c77),c79),f19(f21(c83,c77),c79))
| ~ p14(f23(f26(c84,c85),c81),c81)
| ~ p68(f19(f21(c83,c77),c79),f23(f26(c84,c85),c81))
| p68(f19(f21(c83,c77),c79),c81) ),
inference(instantiation,[status(thm)],[96]) ).
cnf(l46,plain,
p7(f19(f21(c83,c77),c79),f19(f21(c83,c77),c79)),
inference(instantiation,[status(thm)],[2]) ).
cnf(45,plain,
~ p68(f19(f21(c83,c77),c79),c81),
inference(cnf,[status(esa)],[not_p68_46]) ).
cnf(l42,plain,
~ p68(f19(f21(c83,c77),c79),c81),
inference(instantiation,[status(thm)],[45]) ).
cnf(42,plain,
p70(f30(c88,X0),f38(c85,X1)),
inference(cnf,[status(esa)],[p70_43]) ).
cnf(l43,plain,
p70(f30(c88,f32(c89,f8(c75,c76))),f38(c85,f40(f42(f44(f46(c87,c79),f23(f26(c84,c85),c81)),c85),f23(f26(c84,c85),c81)))),
inference(instantiation,[status(thm)],[42]) ).
cnf(l45,plain,
p14(f23(f26(c84,c85),c81),c81),
inference(instantiation,[status(thm)],[44]) ).
cnf(89,plain,
( ~ p14(X0,X1)
| ~ p14(X0,X2)
| p14(X1,X2) ),
inference(cnf,[status(esa)],[p14_90]) ).
cnf(l47,plain,
( ~ p14(f23(f26(c84,c85),f23(f26(c84,c85),c81)),f23(f26(c84,c85),c81))
| ~ p14(f23(f26(c84,c85),f23(f26(c84,c85),c81)),f23(f26(c84,c85),f23(f26(c84,c85),c81)))
| p14(f23(f26(c84,c85),c81),f23(f26(c84,c85),f23(f26(c84,c85),c81))) ),
inference(instantiation,[status(thm)],[89]) ).
cnf(l50,plain,
p14(f23(f26(c84,c85),f23(f26(c84,c85),c81)),f23(f26(c84,c85),c81)),
inference(instantiation,[status(thm)],[44]) ).
cnf(37,plain,
p14(X0,X0),
inference(cnf,[status(esa)],[p14_38]) ).
cnf(l49,plain,
p14(f23(f26(c84,c85),f23(f26(c84,c85),c81)),f23(f26(c84,c85),f23(f26(c84,c85),c81))),
inference(instantiation,[status(thm)],[37]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l16,l17,l21,l3,l18,l25,l19,l27,l22,l41,l46,l42,l43,l45,l47,l50,l49]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN719-1 : TPTP v9.0.0. Released v2.5.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.33 % Computer : n028.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Tue Jul 22 17:47:04 EDT 2025
% 0.13/0.33 % CPUTime :
% 0.13/0.34 % launching worker at depth: 1
% 0.13/0.34 % launching worker at depth: 8
% 0.13/0.34 % launching worker at depth: 3
% 0.13/0.34 % launching worker at depth: 4
% 0.13/0.34 % launching worker at depth: 5
% 0.13/0.34 % launching worker at depth: 6
% 0.13/0.34 % launching worker at depth: 7
% 0.13/0.34 % launching worker at depth: 2
% 0.18/0.34 % launching worker at depth: 9
% 0.18/0.38 % launching worker at depth: 10
% 0.18/0.38 % SZS status Theorem for theBenchmark
% 0.18/0.38 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------