%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : GEO344+1 : TPTP v9.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 6.27s 1.15s
% Output : CNFRefutation 6.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO344+1 : TPTP v9.0.0. Released v4.1.0.
% 0.03/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.33 % Computer : n020.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 : Sun Jul 20 12:09:04 EDT 2025
% 0.13/0.33 % CPUTime :
% 0.13/0.36 % launching worker at depth: 1
% 0.13/0.36 % launching worker at depth: 3
% 0.13/0.36 % launching worker at depth: 5
% 0.13/0.36 % launching worker at depth: 2
% 0.13/0.36 % launching worker at depth: 7
% 0.13/0.36 % launching worker at depth: 6
% 0.13/0.36 % launching worker at depth: 8
% 0.13/0.36 % launching worker at depth: 4
% 0.20/0.38 % launching worker at depth: 9
% 6.27/1.15 % SZS status Theorem for theBenchmark
% 6.27/1.15 % SZS output start CNFRefutation
% 6.27/1.15 fof('qu(theu(the(409), 1), imp(the(409)))', plain, ![Vdthex]:((ron(vd1409,Vdthex)&ron(vd1401,Vdthex)&rline(Vdthex))=>Vdthex=vd1419), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'qu(theu(the(409), 1), imp(the(409)))')).
% 6.27/1.15 fof('qu(theu(the(409), 1), imp(the(409)))'_negated, plain, ~(![Vdthex]:((ron(vd1409,Vdthex)&ron(vd1401,Vdthex)&rline(Vdthex))=>Vdthex=vd1419)), inference(negate_conjecture, [status(cth)], ['qu(theu(the(409), 1), imp(the(409)))'])).
% 6.27/1.15 cnf(0, plain, ron(vd1409,sK1), inference(cnf, [status(esa)], ['qu(theu(the(409), 1), imp(the(409)))'_negated])).
% 6.27/1.15 cnf(l0, plain, ron(vd1409,sK1), inference(instantiation, [status(thm)], [0])).
% 6.27/1.15 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/sandbox/benchmark/theBenchmark.p', 'qu(cond(axiom(73), 0), imp(cond(axiom(73), 0)))')).
% 6.27/1.15 cnf(35, plain, ~ron(X0,X1) | ~ron(X0,X2) | ~ron(X3,X1) | ~ron(X3,X2) | ~rline(X4) | ~rline(X5) | X0 != X6 | X3 != X7 | X1 != X5 | X2 != X4 | ~rpoint(X7) | ~rpoint(X6) | X0 = X3 | X1 = X2, inference(cnf, [status(esa)], ['qu(cond(axiom(73), 0), imp(cond(axiom(73), 0)))'])).
% 6.27/1.15 cnf(l1, plain, ~ron(vd1409,sK1) | ~ron(vd1409,vd1419) | ~ron(vd1401,sK1) | ~ron(vd1401,vd1419) | ~rline(vd1419) | ~rline(sK1) | vd1409 != vd1409 | vd1401 != sK2 | sK1 != sK1 | vd1419 != vd1419 | ~rpoint(sK2) | ~rpoint(vd1409) | vd1409 = vd1401 | sK1 = vd1419, inference(instantiation, [status(thm)], [35])).
% 6.27/1.15 cnf(2, plain, rline(sK1), inference(cnf, [status(esa)], ['qu(theu(the(409), 1), imp(the(409)))'_negated])).
% 6.27/1.15 cnf(l10, plain, rline(sK1), inference(instantiation, [status(thm)], [2])).
% 6.27/1.15 fof('and(pred(s2(plural(the(409))), 0), and(pred(s1(plural(the(409))), 0), pred(the(409), 0)))', plain, (ron(vd1409,vd1419)&ron(vd1401,vd1419)&rline(vd1419)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'and(pred(s2(plural(the(409))), 0), and(pred(s1(plural(the(409))), 0), pred(the(409), 0)))')).
% 6.27/1.15 cnf(5, plain, ron(vd1401,vd1419), inference(cnf, [status(esa)], ['and(pred(s2(plural(the(409))), 0), and(pred(s1(plural(the(409))), 0), pred(the(409), 0)))'])).
% 6.27/1.15 cnf(l4, plain, ron(vd1401,vd1419), inference(instantiation, [status(thm)], [5])).
% 6.27/1.15 cnf(1, plain, ron(vd1401,sK1), inference(cnf, [status(esa)], ['qu(theu(the(409), 1), imp(the(409)))'_negated])).
% 6.27/1.15 cnf(l19, plain, ron(vd1401,sK1), inference(instantiation, [status(thm)], [1])).
% 6.27/1.15 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/sandbox/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))))))))))))')).
% 6.27/1.15 cnf(22, 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))))))))))))'])).
% 6.27/1.15 cnf(l20, plain, rpoint(sK2), inference(instantiation, [status(thm)], [22])).
% 6.27/1.15 cnf(21, 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))))))))))))'])).
% 6.27/1.15 cnf(l7, plain, vd1401 = sK2, inference(instantiation, [status(thm)], [21])).
% 6.27/1.15 cnf(6, plain, rline(vd1419), inference(cnf, [status(esa)], ['and(pred(s2(plural(the(409))), 0), and(pred(s1(plural(the(409))), 0), pred(the(409), 0)))'])).
% 6.27/1.15 cnf(l3, plain, rline(vd1419), inference(instantiation, [status(thm)], [6])).
% 6.27/1.15 fof('pred(406, 0)', plain, rpoint(vd1409), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'pred(406, 0)')).
% 6.27/1.15 cnf(13, plain, rpoint(vd1409), inference(cnf, [status(esa)], ['pred(406, 0)'])).
% 6.27/1.15 cnf(l23, plain, rpoint(vd1409), inference(instantiation, [status(thm)], [13])).
% 6.27/1.15 fof('holds(conjunct2(conjunct2(conjunct2(406))), 1413, 0)', plain, vd1409!=vd1401, file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'holds(conjunct2(conjunct2(conjunct2(406))), 1413, 0)')).
% 6.27/1.15 cnf(12, plain, vd1409 != vd1401, inference(cnf, [status(esa)], ['holds(conjunct2(conjunct2(conjunct2(406))), 1413, 0)'])).
% 6.27/1.15 cnf(l13, plain, vd1409 != vd1401, inference(instantiation, [status(thm)], [12])).
% 6.27/1.15 cnf(4, plain, ron(vd1409,vd1419), inference(cnf, [status(esa)], ['and(pred(s2(plural(the(409))), 0), and(pred(s1(plural(the(409))), 0), pred(the(409), 0)))'])).
% 6.27/1.15 cnf(l26, plain, ron(vd1409,vd1419), inference(instantiation, [status(thm)], [4])).
% 6.27/1.15 cnf(3, plain, sK1 != vd1419, inference(cnf, [status(esa)], ['qu(theu(the(409), 1), imp(the(409)))'_negated])).
% 6.27/1.15 cnf(l12, plain, sK1 != vd1419, inference(instantiation, [status(thm)], [3])).
% 6.27/1.15 cnf(final, plain, $false, inference(ground_refutation, [status(thm)], [l0, l1, l10, l4, l19, l20, l7, l3, l23, l13, l26, l12])).
% 6.27/1.15 % SZS output end CNFRefutation
%------------------------------------------------------------------------------