%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : GEO343+1 : TPTP v9.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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 : Thu Jul 24 01:38:55 PM UTC 2025
% Result : Theorem 8.23s 1.41s
% Output : CNFRefutation 8.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : GEO343+1 : TPTP v9.0.0. Released v4.1.0.
% 0.10/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n017.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jul 20 12:09:19 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.36 % launching worker at depth: 3
% 0.12/0.36 % launching worker at depth: 8
% 0.12/0.36 % launching worker at depth: 2
% 0.12/0.36 % launching worker at depth: 4
% 0.12/0.36 % launching worker at depth: 5
% 0.12/0.36 % launching worker at depth: 6
% 0.12/0.36 % launching worker at depth: 7
% 0.12/0.36 % launching worker at depth: 1
% 0.12/0.38 % launching worker at depth: 9
% 8.23/1.41 % SZS status Theorem for theBenchmark
% 8.23/1.41 % SZS output start CNFRefutation
% 8.23/1.41 fof('qu(theu(the(408), 1), imp(the(408)))', plain, ![Vdthex]:((ron(vd1399,Vdthex)&ron(vd1401,Vdthex)&rline(Vdthex))=>Vdthex=vd1416), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'qu(theu(the(408), 1), imp(the(408)))')).
% 8.23/1.41 fof('qu(theu(the(408), 1), imp(the(408)))'_negated, plain, ~(![Vdthex]:((ron(vd1399,Vdthex)&ron(vd1401,Vdthex)&rline(Vdthex))=>Vdthex=vd1416)), inference(negate_conjecture, [status(cth)], ['qu(theu(the(408), 1), imp(the(408)))'])).
% 8.23/1.41 cnf(0, plain, ron(vd1399,sK1), inference(cnf, [status(esa)], ['qu(theu(the(408), 1), imp(the(408)))'_negated])).
% 8.23/1.41 cnf(l0, plain, ron(vd1399,sK1), inference(instantiation, [status(thm)], [0])).
% 8.23/1.41 fof('qu(cond(axiom(73), 0), imp(cond(axiom(73), 0)))', plain, ![Vd314,Vd315,Vd319,Vd320]:((ron(Vd315,Vd320)&ron(Vd315,Vd319)&ron(Vd314,Vd320)&ron(Vd314,Vd319)&?[Vd324]:(Vd320=Vd324&rline(Vd324))&?[Vd323]:(Vd319=Vd323&rline(Vd323))&Vd314!=Vd315&?[Vd318]:(Vd315=Vd318&rpoint(Vd318))&?[Vd317]:(Vd314=Vd317&rpoint(Vd317)))=>Vd319=Vd320), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'qu(cond(axiom(73), 0), imp(cond(axiom(73), 0)))')).
% 8.23/1.41 cnf(109, plain, ~ron(X0,X1) | ~ron(X0,X2) | ~ron(X3,X1) | ~ron(X3,X2) | ~rpoint(X4) | ~rpoint(X5) | ~rline(X6) | ~rline(X7) | X0 != X5 | X3 != X4 | X1 != X7 | X2 != X6 | X0 = X3 | X1 = X2, inference(cnf, [status(esa)], ['qu(cond(axiom(73), 0), imp(cond(axiom(73), 0)))'])).
% 8.23/1.41 cnf(l1, plain, ~ron(vd1399,sK1) | ~ron(vd1399,vd1416) | ~ron(vd1401,sK1) | ~ron(vd1401,vd1416) | ~rpoint(sK2) | ~rpoint(sK4) | ~rline(vd1416) | ~rline(sK1) | vd1399 != sK4 | vd1401 != sK2 | sK1 != sK1 | vd1416 != vd1416 | vd1399 = vd1401 | sK1 = vd1416, inference(instantiation, [status(thm)], [109])).
% 8.23/1.41 fof('and(pred(conjunct2(405), 5), and(pred(s2(plural(conjunct2(405))), 0), and(pred(s1(plural(conjunct2(405))), 0), and(pred(conjunct2(405), 1), and(pred(conjunct1(405), 9), and(pred(conjunct1(405), 8), and(pred(conjunct1(405), 7), and(qe(s3(plural(405))), and(qe(s2(plural(405))), qe(s1(plural(405))))))))))))', plain, (vd1406=vd1407&ron(vd1400,vd1406)&ron(vd1399,vd1406)&rline(vd1407)&vd1400!=vd1401&vd1399!=vd1401&vd1399!=vd1400&?[Vd1405]:(vd1401=Vd1405&rpoint(Vd1405))&?[Vd1404]:(vd1400=Vd1404&rpoint(Vd1404))&?[Vd1403]:(vd1399=Vd1403&rpoint(Vd1403))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'and(pred(conjunct2(405), 5), and(pred(s2(plural(conjunct2(405))), 0), and(pred(s1(plural(conjunct2(405))), 0), and(pred(conjunct2(405), 1), and(pred(conjunct1(405), 9), and(pred(conjunct1(405), 8), and(pred(conjunct1(405), 7), and(qe(s3(plural(405))), and(qe(s2(plural(405))), qe(s1(plural(405))))))))))))')).
% 8.23/1.41 cnf(16, plain, rpoint(sK2), inference(cnf, [status(esa)], ['and(pred(conjunct2(405), 5), and(pred(s2(plural(conjunct2(405))), 0), and(pred(s1(plural(conjunct2(405))), 0), and(pred(conjunct2(405), 1), and(pred(conjunct1(405), 9), and(pred(conjunct1(405), 8), and(pred(conjunct1(405), 7), and(qe(s3(plural(405))), and(qe(s2(plural(405))), qe(s1(plural(405))))))))))))'])).
% 8.23/1.41 cnf(l25, plain, rpoint(sK2), inference(instantiation, [status(thm)], [16])).
% 8.23/1.41 cnf(15, plain, vd1401 = sK2, inference(cnf, [status(esa)], ['and(pred(conjunct2(405), 5), and(pred(s2(plural(conjunct2(405))), 0), and(pred(s1(plural(conjunct2(405))), 0), and(pred(conjunct2(405), 1), and(pred(conjunct1(405), 9), and(pred(conjunct1(405), 8), and(pred(conjunct1(405), 7), and(qe(s3(plural(405))), and(qe(s2(plural(405))), qe(s1(plural(405))))))))))))'])).
% 8.23/1.41 cnf(l18, plain, vd1401 = sK2, inference(instantiation, [status(thm)], [15])).
% 8.23/1.41 cnf(2, plain, rline(sK1), inference(cnf, [status(esa)], ['qu(theu(the(408), 1), imp(the(408)))'_negated])).
% 8.23/1.41 cnf(l26, plain, rline(sK1), inference(instantiation, [status(thm)], [2])).
% 8.23/1.41 cnf(3, plain, sK1 != vd1416, inference(cnf, [status(esa)], ['qu(theu(the(408), 1), imp(the(408)))'_negated])).
% 8.23/1.41 cnf(l4, plain, sK1 != vd1416, inference(instantiation, [status(thm)], [3])).
% 8.23/1.41 cnf(19, plain, vd1399 = sK4, inference(cnf, [status(esa)], ['and(pred(conjunct2(405), 5), and(pred(s2(plural(conjunct2(405))), 0), and(pred(s1(plural(conjunct2(405))), 0), and(pred(conjunct2(405), 1), and(pred(conjunct1(405), 9), and(pred(conjunct1(405), 8), and(pred(conjunct1(405), 7), and(qe(s3(plural(405))), and(qe(s2(plural(405))), qe(s1(plural(405))))))))))))'])).
% 8.23/1.41 cnf(l20, plain, vd1399 = sK4, inference(instantiation, [status(thm)], [19])).
% 8.23/1.41 cnf(20, plain, rpoint(sK4), inference(cnf, [status(esa)], ['and(pred(conjunct2(405), 5), and(pred(s2(plural(conjunct2(405))), 0), and(pred(s1(plural(conjunct2(405))), 0), and(pred(conjunct2(405), 1), and(pred(conjunct1(405), 9), and(pred(conjunct1(405), 8), and(pred(conjunct1(405), 7), and(qe(s3(plural(405))), and(qe(s2(plural(405))), qe(s1(plural(405))))))))))))'])).
% 8.23/1.41 cnf(l16, plain, rpoint(sK4), inference(instantiation, [status(thm)], [20])).
% 8.23/1.41 fof('and(pred(s2(plural(the(408))), 0), and(pred(s1(plural(the(408))), 0), pred(the(408), 0)))', plain, (ron(vd1399,vd1416)&ron(vd1401,vd1416)&rline(vd1416)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'and(pred(s2(plural(the(408))), 0), and(pred(s1(plural(the(408))), 0), pred(the(408), 0)))')).
% 8.23/1.41 cnf(5, plain, ron(vd1401,vd1416), inference(cnf, [status(esa)], ['and(pred(s2(plural(the(408))), 0), and(pred(s1(plural(the(408))), 0), pred(the(408), 0)))'])).
% 8.23/1.41 cnf(l27, plain, ron(vd1401,vd1416), inference(instantiation, [status(thm)], [5])).
% 8.23/1.41 cnf(6, plain, rline(vd1416), inference(cnf, [status(esa)], ['and(pred(s2(plural(the(408))), 0), and(pred(s1(plural(the(408))), 0), pred(the(408), 0)))'])).
% 8.23/1.41 cnf(l28, plain, rline(vd1416), inference(instantiation, [status(thm)], [6])).
% 8.23/1.41 cnf(4, plain, ron(vd1399,vd1416), inference(cnf, [status(esa)], ['and(pred(s2(plural(the(408))), 0), and(pred(s1(plural(the(408))), 0), pred(the(408), 0)))'])).
% 8.23/1.41 cnf(l24, plain, ron(vd1399,vd1416), inference(instantiation, [status(thm)], [4])).
% 8.23/1.41 cnf(13, plain, vd1399 != vd1401, inference(cnf, [status(esa)], ['and(pred(conjunct2(405), 5), and(pred(s2(plural(conjunct2(405))), 0), and(pred(s1(plural(conjunct2(405))), 0), and(pred(conjunct2(405), 1), and(pred(conjunct1(405), 9), and(pred(conjunct1(405), 8), and(pred(conjunct1(405), 7), and(qe(s3(plural(405))), and(qe(s2(plural(405))), qe(s1(plural(405))))))))))))'])).
% 8.23/1.41 cnf(l12, plain, vd1399 != vd1401, inference(instantiation, [status(thm)], [13])).
% 8.23/1.41 cnf(1, plain, ron(vd1401,sK1), inference(cnf, [status(esa)], ['qu(theu(the(408), 1), imp(the(408)))'_negated])).
% 8.23/1.41 cnf(l22, plain, ron(vd1401,sK1), inference(instantiation, [status(thm)], [1])).
% 8.23/1.41 cnf(final, plain, $false, inference(ground_refutation, [status(thm)], [l0, l1, l25, l18, l26, l4, l20, l16, l27, l28, l24, l12, l22])).
% 8.23/1.41 % SZS output end CNFRefutation
%------------------------------------------------------------------------------