%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : GEO305+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 : 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 : Thu Jul 24 01:38:52 PM UTC 2025
% Result : Theorem 0.18s 0.49s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO305+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.12/0.33 % Computer : n028.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:00:04 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.36 % launching worker at depth: 3
% 0.12/0.36 % launching worker at depth: 4
% 0.12/0.36 % launching worker at depth: 1
% 0.12/0.36 % launching worker at depth: 2
% 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: 8
% 0.12/0.36 % launching worker at depth: 9
% 0.18/0.49 % SZS status Theorem for theBenchmark
% 0.18/0.49 % SZS output start CNFRefutation
% 0.18/0.49 fof('pred(conjunct2(349), 0)', plain, ron(vd1302,vd1297), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'pred(conjunct2(349), 0)')).
% 0.18/0.49 fof('pred(conjunct2(349), 0)'_negated, plain, ~(ron(vd1302,vd1297)), inference(negate_conjecture, [status(cth)], ['pred(conjunct2(349), 0)'])).
% 0.18/0.49 cnf(0, plain, ~ron(vd1302,vd1297), inference(cnf, [status(esa)], ['pred(conjunct2(349), 0)'_negated])).
% 0.18/0.49 cnf(l0, plain, ~ron(vd1302,vd1297), inference(instantiation, [status(thm)], [0])).
% 0.18/0.49 fof('qu(cond(axiom(83), 0), imp(cond(axiom(83), 0)))', plain, ![Vd352,Vd353,Vd354,Vd359,Vd360]:((Vd359=Vd360&ron(Vd353,Vd359)&ron(Vd352,Vd359)&rR(Vd353,Vd352,Vd354)&rline(Vd360)&?[Vd358]:(Vd354=Vd358&rpoint(Vd358))&?[Vd357]:(Vd353=Vd357&rpoint(Vd357))&?[Vd356]:(Vd352=Vd356&rpoint(Vd356)))=>ron(Vd354,Vd359)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'qu(cond(axiom(83), 0), imp(cond(axiom(83), 0)))')).
% 0.18/0.49 cnf(24, plain, ~ron(X0,X1) | ~ron(X2,X1) | X0 != X3 | X2 != X4 | X5 != X6 | X1 != X7 | ~rR(X2,X0,X5) | ~rpoint(X6) | ~rpoint(X4) | ~rpoint(X3) | ~rline(X7) | ron(X5,X1), inference(cnf, [status(esa)], ['qu(cond(axiom(83), 0), imp(cond(axiom(83), 0)))'])).
% 0.18/0.49 cnf(l1, plain, ~ron(vd1287,vd1297) | ~ron(vd1289,vd1297) | vd1287 != sK3 | vd1289 != sK1 | vd1302 != vd1303 | vd1297 != vd1297 | ~rR(vd1289,vd1287,vd1302) | ~rpoint(vd1303) | ~rpoint(sK1) | ~rpoint(sK3) | ~rline(vd1297) | ron(vd1302,vd1297), inference(instantiation, [status(thm)], [24])).
% 0.18/0.49 fof('pred(s2(plural(347)), 0)', plain, ron(vd1289,vd1297), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'pred(s2(plural(347)), 0)')).
% 0.18/0.49 cnf(8, plain, ron(vd1289,vd1297), inference(cnf, [status(esa)], ['pred(s2(plural(347)), 0)'])).
% 0.18/0.49 cnf(l34, plain, ron(vd1289,vd1297), inference(instantiation, [status(thm)], [8])).
% 0.18/0.49 fof('and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))', plain, (vf(vd1287,vd1288)=vf(vd1287,vd1289)&vd1288!=vd1289&vd1287!=vd1289&vd1287!=vd1288&?[Vd1293]:(vd1289=Vd1293&rpoint(Vd1293))&?[Vd1292]:(vd1288=Vd1292&rpoint(Vd1292))&?[Vd1291]:(vd1287=Vd1291&rpoint(Vd1291))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))')).
% 0.18/0.49 cnf(18, plain, vd1289 = sK1, inference(cnf, [status(esa)], ['and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))'])).
% 0.18/0.49 cnf(l30, plain, vd1289 = sK1, inference(instantiation, [status(thm)], [18])).
% 0.18/0.49 fof('pred(347, 0)', plain, rline(vd1297), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'pred(347, 0)')).
% 0.18/0.49 cnf(10, plain, rline(vd1297), inference(cnf, [status(esa)], ['pred(347, 0)'])).
% 0.18/0.49 cnf(l2, plain, rline(vd1297), inference(instantiation, [status(thm)], [10])).
% 0.18/0.49 cnf(22, plain, vd1287 = sK3, inference(cnf, [status(esa)], ['and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))'])).
% 0.18/0.49 cnf(l19, plain, vd1287 = sK3, inference(instantiation, [status(thm)], [22])).
% 0.18/0.49 fof('pred(s1(plural(347)), 0)', plain, ron(vd1287,vd1297), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'pred(s1(plural(347)), 0)')).
% 0.18/0.49 cnf(9, plain, ron(vd1287,vd1297), inference(cnf, [status(esa)], ['pred(s1(plural(347)), 0)'])).
% 0.18/0.49 cnf(l39, plain, ron(vd1287,vd1297), inference(instantiation, [status(thm)], [9])).
% 0.18/0.49 cnf(19, plain, rpoint(sK1), inference(cnf, [status(esa)], ['and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))'])).
% 0.18/0.49 cnf(l17, plain, rpoint(sK1), inference(instantiation, [status(thm)], [19])).
% 0.18/0.49 fof('and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))', plain, (vd1302=vd1303&rR(vd1289,vd1287,vd1302)&rpoint(vd1303)&rR(vd1288,vd1287,vd1299)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))')).
% 0.18/0.49 cnf(4, plain, rR(vd1289,vd1287,vd1302), inference(cnf, [status(esa)], ['and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))'])).
% 0.18/0.49 cnf(l20, plain, rR(vd1289,vd1287,vd1302), inference(instantiation, [status(thm)], [4])).
% 0.18/0.49 cnf(3, plain, vd1302 = vd1303, inference(cnf, [status(esa)], ['and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))'])).
% 0.18/0.49 cnf(l25, plain, vd1302 = vd1303, inference(instantiation, [status(thm)], [3])).
% 0.18/0.49 cnf(23, plain, rpoint(sK3), inference(cnf, [status(esa)], ['and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))'])).
% 0.18/0.49 cnf(l14, plain, rpoint(sK3), inference(instantiation, [status(thm)], [23])).
% 0.18/0.49 cnf(5, plain, rpoint(vd1303), inference(cnf, [status(esa)], ['and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))'])).
% 0.18/0.49 cnf(l24, plain, rpoint(vd1303), inference(instantiation, [status(thm)], [5])).
% 0.18/0.49 cnf(final, plain, $false, inference(ground_refutation, [status(thm)], [l0, l1, l34, l30, l2, l19, l39, l17, l20, l25, l14, l24])).
% 0.18/0.49 % SZS output end CNFRefutation
%------------------------------------------------------------------------------