%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : GEO340+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 : n021.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 5.58s 1.10s
% Output : CNFRefutation 5.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO340+1 : TPTP v9.0.0. Released v4.1.0.
% 0.07/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Sun Jul 20 12:08:49 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.37 % launching worker at depth: 1
% 0.13/0.37 % launching worker at depth: 4
% 0.13/0.37 % launching worker at depth: 3
% 0.13/0.37 % launching worker at depth: 2
% 0.13/0.37 % launching worker at depth: 5
% 0.13/0.37 % launching worker at depth: 6
% 0.13/0.37 % launching worker at depth: 7
% 0.13/0.37 % launching worker at depth: 8
% 0.21/0.45 % launching worker at depth: 9
% 5.58/1.10 % SZS status Theorem for theBenchmark
% 5.58/1.10 % SZS output start CNFRefutation
% 5.58/1.10 fof('neg(neg(403))', plain, ~?[Vd1394]:(Vd1394!=vd1386&vf(vd1385,vd1386)=vf(vd1385,Vd1394)&vf(vd1384,vd1386)=vf(vd1384,Vd1394)&rS(vd1386,Vd1394,vd1391)&rpoint(Vd1394)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'neg(neg(403))')).
% 5.58/1.10 fof('neg(neg(403))'_negated, plain, ~(~?[Vd1394]:(Vd1394!=vd1386&vf(vd1385,vd1386)=vf(vd1385,Vd1394)&vf(vd1384,vd1386)=vf(vd1384,Vd1394)&rS(vd1386,Vd1394,vd1391)&rpoint(Vd1394))), inference(negate_conjecture, [status(cth)], ['neg(neg(403))'])).
% 5.58/1.10 cnf(0, plain, sK1 != vd1386, inference(cnf, [status(esa)], ['neg(neg(403))'_negated])).
% 5.58/1.10 cnf(l0, plain, sK1 != vd1386, inference(instantiation, [status(thm)], [0])).
% 5.58/1.10 fof('ass(cond(proof(404), 0), 0)', plain, ![Vd1399,Vd1400,Vd1401,Vd1406,Vd1407]:((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)))=>![Vd1409]:((Vd1409!=Vd1401&vf(Vd1400,Vd1401)=vf(Vd1400,Vd1409)&vf(Vd1399,Vd1401)=vf(Vd1399,Vd1409)&rS(Vd1401,Vd1409,Vd1406)&rpoint(Vd1409))=>![Vd1415]:(Vd1415=vskolem1416(Vd1409,Vd1399,Vd1400,Vd1401,Vd1406,Vd1407)=>![Vd1418]:Vd1418!=vskolem1419(Vd1415,Vd1409,Vd1399,Vd1400,Vd1401,Vd1406,Vd1407)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'ass(cond(proof(404), 0), 0)')).
% 5.58/1.10 cnf(18, plain, X0 != X1 | X2 != X3 | X4 != X5 | X6 != X7 | X8 != vskolem1416(X9,X0,X2,X4,X6,X7) | X10 != vskolem1419(X8,X9,X0,X2,X4,X6,X7) | vf(X0,X4) != vf(X0,X9) | vf(X2,X4) != vf(X2,X9) | ~rS(X4,X9,X6) | ~rpoint(X5) | ~rpoint(X3) | ~rpoint(X1) | ~rpoint(X9) | ~ron(X0,X6) | ~ron(X2,X6) | ~rline(X7) | X0 = X2 | X0 = X4 | X2 = X4 | X9 = X4, inference(cnf, [status(esa)], ['ass(cond(proof(404), 0), 0)'])).
% 5.58/1.10 cnf(l1, plain, vd1384 != sK4 | vd1385 != sK3 | vd1386 != sK2 | vd1391 != vd1392 | vskolem1416(sK1,vd1384,vd1385,vd1386,vd1391,vd1392) != vskolem1416(sK1,vd1384,vd1385,vd1386,vd1391,vd1392) | vskolem1419(vskolem1416(sK1,vd1384,vd1385,vd1386,vd1391,vd1392),sK1,vd1384,vd1385,vd1386,vd1391,vd1392) != vskolem1419(vskolem1416(sK1,vd1384,vd1385,vd1386,vd1391,vd1392),sK1,vd1384,vd1385,vd1386,vd1391,vd1392) | vf(vd1384,vd1386) != vf(vd1384,sK1) | vf(vd1385,vd1386) != vf(vd1385,sK1) | ~rS(vd1386,sK1,vd1391) | ~rpoint(sK2) | ~rpoint(sK3) | ~rpoint(sK4) | ~rpoint(sK1) | ~ron(vd1384,vd1391) | ~ron(vd1385,vd1391) | ~rline(vd1392) | vd1384 = vd1385 | vd1384 = vd1386 | vd1385 = vd1386 | sK1 = vd1386, inference(instantiation, [status(thm)], [18])).
% 5.58/1.10 cnf(1, plain, vf(vd1385,vd1386) = vf(vd1385,sK1), inference(cnf, [status(esa)], ['neg(neg(403))'_negated])).
% 5.58/1.10 cnf(l8, plain, vf(vd1385,vd1386) = vf(vd1385,sK1), inference(instantiation, [status(thm)], [1])).
% 5.58/1.10 fof('and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))', plain, (vd1391=vd1392&ron(vd1385,vd1391)&ron(vd1384,vd1391)&rline(vd1392)&vd1385!=vd1386&vd1384!=vd1386&vd1384!=vd1385&?[Vd1390]:(vd1386=Vd1390&rpoint(Vd1390))&?[Vd1389]:(vd1385=Vd1389&rpoint(Vd1389))&?[Vd1388]:(vd1384=Vd1388&rpoint(Vd1388))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))')).
% 5.58/1.10 cnf(7, plain, ron(vd1384,vd1391), inference(cnf, [status(esa)], ['and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))'])).
% 5.58/1.10 cnf(l12, plain, ron(vd1384,vd1391), inference(instantiation, [status(thm)], [7])).
% 5.58/1.10 cnf(6, plain, ron(vd1385,vd1391), inference(cnf, [status(esa)], ['and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))'])).
% 5.58/1.10 cnf(l19, plain, ron(vd1385,vd1391), inference(instantiation, [status(thm)], [6])).
% 5.58/1.10 cnf(2, plain, vf(vd1384,vd1386) = vf(vd1384,sK1), inference(cnf, [status(esa)], ['neg(neg(403))'_negated])).
% 5.58/1.10 cnf(l4, plain, vf(vd1384,vd1386) = vf(vd1384,sK1), inference(instantiation, [status(thm)], [2])).
% 5.58/1.10 cnf(12, plain, vd1386 = sK2, inference(cnf, [status(esa)], ['and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))'])).
% 5.58/1.10 cnf(l6, plain, vd1386 = sK2, inference(instantiation, [status(thm)], [12])).
% 5.58/1.10 cnf(4, plain, rpoint(sK1), inference(cnf, [status(esa)], ['neg(neg(403))'_negated])).
% 5.58/1.10 cnf(l13, plain, rpoint(sK1), inference(instantiation, [status(thm)], [4])).
% 5.58/1.10 cnf(3, plain, rS(vd1386,sK1,vd1391), inference(cnf, [status(esa)], ['neg(neg(403))'_negated])).
% 5.58/1.10 cnf(l5, plain, rS(vd1386,sK1,vd1391), inference(instantiation, [status(thm)], [3])).
% 5.58/1.10 cnf(13, plain, rpoint(sK2), inference(cnf, [status(esa)], ['and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))'])).
% 5.58/1.10 cnf(l18, plain, rpoint(sK2), inference(instantiation, [status(thm)], [13])).
% 5.58/1.10 cnf(5, plain, vd1391 = vd1392, inference(cnf, [status(esa)], ['and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))'])).
% 5.58/1.10 cnf(l11, plain, vd1391 = vd1392, inference(instantiation, [status(thm)], [5])).
% 5.58/1.10 cnf(14, plain, vd1385 = sK3, inference(cnf, [status(esa)], ['and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))'])).
% 5.58/1.10 cnf(l3, plain, vd1385 = sK3, inference(instantiation, [status(thm)], [14])).
% 5.58/1.10 cnf(8, plain, rline(vd1392), inference(cnf, [status(esa)], ['and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))'])).
% 5.58/1.10 cnf(l17, plain, rline(vd1392), inference(instantiation, [status(thm)], [8])).
% 5.58/1.10 cnf(16, plain, vd1384 = sK4, inference(cnf, [status(esa)], ['and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))'])).
% 5.58/1.10 cnf(l9, plain, vd1384 = sK4, inference(instantiation, [status(thm)], [16])).
% 5.58/1.10 cnf(17, plain, rpoint(sK4), inference(cnf, [status(esa)], ['and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))'])).
% 5.58/1.10 cnf(l7, plain, rpoint(sK4), inference(instantiation, [status(thm)], [17])).
% 5.58/1.10 cnf(15, plain, rpoint(sK3), inference(cnf, [status(esa)], ['and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))'])).
% 5.58/1.10 cnf(l20, plain, rpoint(sK3), inference(instantiation, [status(thm)], [15])).
% 5.58/1.10 cnf(10, plain, vd1384 != vd1386, inference(cnf, [status(esa)], ['and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))'])).
% 5.58/1.10 cnf(l16, plain, vd1384 != vd1386, inference(instantiation, [status(thm)], [10])).
% 5.58/1.10 cnf(9, plain, vd1385 != vd1386, inference(cnf, [status(esa)], ['and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))'])).
% 5.58/1.10 cnf(l14, plain, vd1385 != vd1386, inference(instantiation, [status(thm)], [9])).
% 5.58/1.10 cnf(11, plain, vd1384 != vd1385, inference(cnf, [status(esa)], ['and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))'])).
% 5.58/1.10 cnf(l33, plain, vd1384 != vd1385, inference(instantiation, [status(thm)], [11])).
% 5.58/1.10 cnf(final, plain, $false, inference(ground_refutation, [status(thm)], [l0, l1, l8, l12, l19, l4, l6, l13, l5, l18, l11, l3, l17, l9, l7, l20, l16, l14, l33])).
% 5.58/1.10 % SZS output end CNFRefutation
%------------------------------------------------------------------------------