%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : GEO279+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:28:04 PM UTC 2026
% Result : Theorem 94.01s 24.18s
% Output : CNFRefutation 94.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 20
% Syntax : Number of formulae : 97 ( 40 unt; 0 def)
% Number of atoms : 481 ( 136 equ)
% Maximal formula atoms : 52 ( 4 avg)
% Number of connectives : 680 ( 296 ~; 293 |; 81 &)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 11 con; 0-7 aty)
% Number of variables : 203 ( 1 sgn 67 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof('qu(cond(axiom(123), 0), imp(cond(axiom(123), 0)))',axiom,
! [X182,X183,X184,X185,X186] :
( ( ? [X189] :
( rpoint(X189)
& X182 = X189 )
& ? [X188] :
( rpoint(X188)
& X183 = X188 )
& ? [X187] :
( rpoint(X187)
& X184 = X187 )
& rcircle(X186)
& X185 = X186
& ( rinside(X182,X185)
| ron(X182,X185) )
& ~ rinside(X184,X185)
& rR(X184,X182,X183) )
=> ( ~ ron(X183,X185)
& ~ ron(X183,X185) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(123), 0), imp(cond(axiom(123), 0)))') ).
fof('qe(s1(plural(224)))',axiom,
? [X25] :
( rpoint(X25)
& vd1080 = X25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(s1(plural(224)))') ).
fof('qu(cond(axiom(186), 0), imp(cond(axiom(186), 0)))',axiom,
! [X717,X718,X719,X720] :
( ( ? [X722] :
( rpoint(X722)
& X717 = X722 )
& ? [X721] :
( rpoint(X721)
& X718 = X721 )
& rcenter(X719,X720)
& ron(X718,X720) )
=> ( rless(vf(X719,X717),vf(X719,X718))
<=> rinside(X717,X720) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(186), 0), imp(cond(axiom(186), 0)))') ).
fof('qu(cond(axiom(1), 0), imp(cond(axiom(1), 0)))',axiom,
! [X548,X549] :
( rcenter(X548,X549)
=> ? [X550,X551] :
( rpoint(X550)
& X548 = X550
& rcircle(X551)
& X549 = X551 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(1), 0), imp(cond(axiom(1), 0)))') ).
fof('holds(conjunct2(comma_conjunct2(229)), 1097, 0)',axiom,
rR(vd1080,vd1089,vd1096),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(comma_conjunct2(229)), 1097, 0)') ).
fof('pred(226, 0)',axiom,
rpoint(vd1089),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(226, 0)') ).
fof('pred(229, 0)',axiom,
rpoint(vd1096),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(229, 0)') ).
fof('qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))',axiom,
! [X45,X46] :
( rcenter(X45,X46)
=> rinside(X45,X46) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))') ).
fof('replace(replace(and(pred(comma_conjunct2(the(231)), 0), and(pred(comma_conjunct1(the(231)), 0), pred(the(231), 0)))))',axiom,
( rcircle(vskolem1102)
& rcenter(vd1089,vskolem1102)
& ron(vd1096,vskolem1102) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','replace(replace(and(pred(comma_conjunct2(the(231)), 0), and(pred(comma_conjunct1(the(231)), 0), pred(the(231), 0)))))') ).
fof('pred(225, 1)',axiom,
rpoint(vd1086),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(225, 1)') ).
fof('pred(225, 4)',axiom,
vd1085 = vd1086,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(225, 4)') ).
fof('qe(232)',conjecture,
? [X1] :
( rpoint(X1)
& ron(X1,vd1101)
& ron(X1,vd1098)
& rR(vd1085,X1,vd1089) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(232)') ).
fof('qu(cond(axiom(63), 0), imp(cond(axiom(63), 0)))',axiom,
! [X9,X10,X11,X12,X13,X14,X15,X16] :
( ( rcircle(X10)
& X9 = X10
& rline(X12)
& X11 = X12
& rpoint(X14)
& X13 = X14
& rinside(X13,X9)
& ron(X13,X11)
& rpoint(X16)
& X15 = X16
& ron(X15,X11)
& X15 != X13 )
=> ? [X17] :
( rpoint(X17)
& ron(X17,X9)
& ron(X17,X11)
& rR(X13,X17,X15) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(63), 0), imp(cond(axiom(63), 0)))') ).
fof('holds(226, 1090, 0)',axiom,
vf(vd1089,vd1085) = vf(vd1089,vd1080),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(226, 1090, 0)') ).
fof('replace(pred(230, 2))',axiom,
vd1098 = vskolem1099,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','replace(pred(230, 2))') ).
fof('replace(pred(231, 2))',axiom,
vd1101 = vskolem1102,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','replace(pred(231, 2))') ).
fof('qu(cond(axiom(162), 0), imp(cond(axiom(162), 0)))',axiom,
! [X61,X62] :
( ( ? [X64] :
( rpoint(X64)
& X61 = X64 )
& ? [X63] :
( rpoint(X63)
& X62 = X63 ) )
=> ( vf(X61,X62) = v0
<=> X61 = X62 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(162), 0), imp(cond(axiom(162), 0)))') ).
fof('holds(conjunct1(225), 1087, 0)',axiom,
vd1085 != vd1080,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(225), 1087, 0)') ).
fof('replace(replace(and(pred(s2(plural(the(230))), 0), and(pred(s1(plural(the(230))), 0), pred(the(230), 0)))))',axiom,
( rline(vskolem1099)
& ron(vd1089,vskolem1099)
& ron(vd1085,vskolem1099) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','replace(replace(and(pred(s2(plural(the(230))), 0), and(pred(s1(plural(the(230))), 0), pred(the(230), 0)))))') ).
fof('holds(226, 1090, 1)',axiom,
vf(vd1089,vd1080) = vf(vd1085,vd1080),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(226, 1090, 1)') ).
fof(c_0_20,plain,
! [X182,X183,X184,X185,X186] :
( ( ? [X189] :
( rpoint(X189)
& X182 = X189 )
& ? [X188] :
( rpoint(X188)
& X183 = X188 )
& ? [X187] :
( rpoint(X187)
& X184 = X187 )
& rcircle(X186)
& X185 = X186
& ( rinside(X182,X185)
| ron(X182,X185) )
& ~ rinside(X184,X185)
& rR(X184,X182,X183) )
=> ~ ron(X183,X185) ),
inference(fof_simplification,[status(thm)],['qu(cond(axiom(123), 0), imp(cond(axiom(123), 0)))']) ).
fof(c_0_21,plain,
! [X927,X928,X929,X930,X931,X932,X933,X934] :
( ( ~ ron(X928,X930)
| ~ rpoint(X934)
| X927 != X934
| ~ rpoint(X933)
| X928 != X933
| ~ rpoint(X932)
| X929 != X932
| ~ rcircle(X931)
| X930 != X931
| rinside(X929,X930)
| ~ rR(X929,X927,X928)
| ~ rinside(X927,X930) )
& ( ~ ron(X928,X930)
| ~ rpoint(X934)
| X927 != X934
| ~ rpoint(X933)
| X928 != X933
| ~ rpoint(X932)
| X929 != X932
| ~ rcircle(X931)
| X930 != X931
| rinside(X929,X930)
| ~ rR(X929,X927,X928)
| ~ ron(X927,X930) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_20])])])])]) ).
fof(c_0_22,plain,
( rpoint(esk2_0)
& vd1080 = esk2_0 ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['qe(s1(plural(224)))'])]) ).
fof(c_0_23,plain,
! [X1462,X1463,X1464,X1465,X1466,X1467] :
( ( ~ rpoint(X1467)
| X1462 != X1467
| ~ rpoint(X1466)
| X1463 != X1466
| ~ rcenter(X1464,X1465)
| ~ ron(X1463,X1465)
| rless(vf(X1464,X1462),vf(X1464,X1463))
| ~ rinside(X1462,X1465) )
& ( ~ rpoint(X1467)
| X1462 != X1467
| ~ rpoint(X1466)
| X1463 != X1466
| ~ rcenter(X1464,X1465)
| ~ ron(X1463,X1465)
| rinside(X1462,X1465)
| ~ rless(vf(X1464,X1462),vf(X1464,X1463)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(186), 0), imp(cond(axiom(186), 0)))'])])])])]) ).
cnf(c_0_24,plain,
( ~ ron(X4,X2)
| ~ rpoint(X8)
| X1 != X8
| ~ rpoint(X7)
| X4 != X7
| ~ rpoint(X6)
| X3 != X6
| ~ rcircle(X5)
| X2 != X5
| ~ rR(X3,X1,X4)
| ~ rinside(X1,X2)
| rinside(X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_25,plain,
rpoint(esk2_0),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_26,plain,
vd1080 = esk2_0,
inference(split_conjunct,[status(thm)],[c_0_22]) ).
fof(c_0_27,plain,
! [X1293,X1294] :
( ( ~ rcenter(X1293,X1294)
| rpoint(esk44_2(X1293,X1294)) )
& ( ~ rcenter(X1293,X1294)
| X1293 = esk44_2(X1293,X1294) )
& ( ~ rcenter(X1293,X1294)
| rcircle(esk45_2(X1293,X1294)) )
& ( ~ rcenter(X1293,X1294)
| X1294 = esk45_2(X1293,X1294) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(1), 0), imp(cond(axiom(1), 0)))'])])])])])]) ).
cnf(c_0_28,plain,
( ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X4 != X5
| ~ rcenter(X3,X2)
| ~ ron(X4,X2)
| ~ rinside(X1,X2)
| rless(vf(X3,X1),vf(X3,X4)) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_29,plain,
( ~ rR(X1,X3,X4)
| ~ ron(X4,X2)
| ~ rpoint(X1)
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rcircle(X2)
| ~ rinside(X3,X2)
| rinside(X1,X2) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_24])])])]) ).
cnf(c_0_30,plain,
rR(vd1080,vd1089,vd1096),
inference(split_conjunct,[status(thm)],['holds(conjunct2(comma_conjunct2(229)), 1097, 0)']) ).
cnf(c_0_31,plain,
rpoint(vd1089),
inference(split_conjunct,[status(thm)],['pred(226, 0)']) ).
cnf(c_0_32,plain,
rpoint(vd1096),
inference(split_conjunct,[status(thm)],['pred(229, 0)']) ).
cnf(c_0_33,plain,
rpoint(vd1080),
inference(rw,[status(thm)],[c_0_25,c_0_26]) ).
cnf(c_0_34,plain,
( ~ rcenter(X1,X2)
| rcircle(esk45_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_35,plain,
( ~ rcenter(X2,X1)
| X1 = esk45_2(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
fof(c_0_36,plain,
! [X781,X782] :
( rinside(X781,X782)
| ~ rcenter(X781,X782) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))'])])]) ).
cnf(c_0_37,plain,
( ~ ron(X3,X4)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rcenter(X1,X4)
| ~ rinside(X2,X4)
| rless(vf(X1,X2),vf(X1,X3)) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_28])]) ).
cnf(c_0_38,plain,
( ~ ron(vd1096,X1)
| ~ rcircle(X1)
| ~ rinside(vd1089,X1)
| rinside(vd1080,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
cnf(c_0_39,plain,
( ~ rcenter(X2,X1)
| rcircle(X1) ),
inference(spm,[status(thm)],[c_0_34,c_0_35]) ).
cnf(c_0_40,plain,
( ~ rcenter(X1,X2)
| rinside(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
cnf(c_0_41,plain,
rcenter(vd1089,vskolem1102),
inference(split_conjunct,[status(thm)],['replace(replace(and(pred(comma_conjunct2(the(231)), 0), and(pred(comma_conjunct1(the(231)), 0), pred(the(231), 0)))))']) ).
cnf(c_0_42,plain,
( ~ rpoint(X6)
| X2 != X6
| ~ rpoint(X5)
| X3 != X5
| ~ rcenter(X1,X4)
| ~ ron(X3,X4)
| ~ rless(vf(X1,X2),vf(X1,X3))
| rinside(X2,X4) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_43,plain,
( ~ ron(X2,X3)
| ~ ron(vd1096,X3)
| ~ rpoint(X2)
| ~ rcenter(X1,X3)
| ~ rinside(vd1089,X3)
| rless(vf(X1,vd1080),vf(X1,X2)) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37,c_0_38]),c_0_33])]),c_0_39]) ).
cnf(c_0_44,plain,
rinside(vd1089,vskolem1102),
inference(spm,[status(thm)],[c_0_40,c_0_41]) ).
cnf(c_0_45,plain,
ron(vd1096,vskolem1102),
inference(split_conjunct,[status(thm)],['replace(replace(and(pred(comma_conjunct2(the(231)), 0), and(pred(comma_conjunct1(the(231)), 0), pred(the(231), 0)))))']) ).
cnf(c_0_46,plain,
( ~ ron(X4,X2)
| ~ rpoint(X4)
| ~ rpoint(X1)
| ~ rcenter(X3,X2)
| ~ rless(vf(X3,X1),vf(X3,X4))
| rinside(X1,X2) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_42])]) ).
cnf(c_0_47,plain,
( ~ ron(X1,vskolem1102)
| ~ rpoint(X1)
| rless(vf(vd1089,vd1080),vf(vd1089,X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43,c_0_41]),c_0_44]),c_0_45])]) ).
cnf(c_0_48,plain,
( ~ ron(X2,X1)
| ~ ron(X2,vskolem1102)
| ~ rpoint(X2)
| ~ rcenter(vd1089,X1)
| rinside(vd1080,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_47]),c_0_33])]) ).
cnf(c_0_49,plain,
rpoint(vd1086),
inference(split_conjunct,[status(thm)],['pred(225, 1)']) ).
cnf(c_0_50,plain,
vd1085 = vd1086,
inference(split_conjunct,[status(thm)],['pred(225, 4)']) ).
cnf(c_0_51,plain,
( ~ ron(X1,vskolem1102)
| ~ rpoint(X1)
| rinside(vd1080,vskolem1102) ),
inference(spm,[status(thm)],[c_0_48,c_0_41]) ).
fof(c_0_52,negated_conjecture,
~ ? [X1] :
( rpoint(X1)
& ron(X1,vd1101)
& ron(X1,vd1098)
& rR(vd1085,X1,vd1089) ),
inference(assume_negation,[status(cth)],['qe(232)']) ).
fof(c_0_53,plain,
! [X9,X10,X11,X12,X13,X14,X15,X16] :
( ( rcircle(X10)
& X9 = X10
& rline(X12)
& X11 = X12
& rpoint(X14)
& X13 = X14
& rinside(X13,X9)
& ron(X13,X11)
& rpoint(X16)
& X15 = X16
& ron(X15,X11)
& X15 != X13 )
=> ? [X17] :
( rpoint(X17)
& ron(X17,X9)
& ron(X17,X11)
& rR(X13,X17,X15) ) ),
inference(fof_simplification,[status(thm)],['qu(cond(axiom(63), 0), imp(cond(axiom(63), 0)))']) ).
cnf(c_0_54,plain,
vf(vd1089,vd1085) = vf(vd1089,vd1080),
inference(split_conjunct,[status(thm)],['holds(226, 1090, 0)']) ).
cnf(c_0_55,plain,
rpoint(vd1085),
inference(rw,[status(thm)],[c_0_49,c_0_50]) ).
cnf(c_0_56,plain,
rinside(vd1080,vskolem1102),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_45]),c_0_32])]) ).
fof(c_0_57,negated_conjecture,
! [X735] :
( ~ rpoint(X735)
| ~ ron(X735,vd1101)
| ~ ron(X735,vd1098)
| ~ rR(vd1085,X735,vd1089) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_52])])]) ).
fof(c_0_58,plain,
! [X743,X744,X745,X746,X747,X748,X749,X750] :
( ( ~ rcircle(X744)
| X743 != X744
| ~ rline(X746)
| X745 != X746
| ~ rpoint(X748)
| X747 != X748
| ~ rinside(X747,X743)
| ~ ron(X747,X745)
| ~ rpoint(X750)
| X749 != X750
| ~ ron(X749,X745)
| X749 = X747
| rpoint(esk1_7(X743,X744,X745,X746,X747,X748,X749)) )
& ( ~ rcircle(X744)
| X743 != X744
| ~ rline(X746)
| X745 != X746
| ~ rpoint(X748)
| X747 != X748
| ~ rinside(X747,X743)
| ~ ron(X747,X745)
| ~ rpoint(X750)
| X749 != X750
| ~ ron(X749,X745)
| X749 = X747
| ron(esk1_7(X743,X744,X745,X746,X747,X748,X749),X743) )
& ( ~ rcircle(X744)
| X743 != X744
| ~ rline(X746)
| X745 != X746
| ~ rpoint(X748)
| X747 != X748
| ~ rinside(X747,X743)
| ~ ron(X747,X745)
| ~ rpoint(X750)
| X749 != X750
| ~ ron(X749,X745)
| X749 = X747
| ron(esk1_7(X743,X744,X745,X746,X747,X748,X749),X745) )
& ( ~ rcircle(X744)
| X743 != X744
| ~ rline(X746)
| X745 != X746
| ~ rpoint(X748)
| X747 != X748
| ~ rinside(X747,X743)
| ~ ron(X747,X745)
| ~ rpoint(X750)
| X749 != X750
| ~ ron(X749,X745)
| X749 = X747
| rR(X747,esk1_7(X743,X744,X745,X746,X747,X748,X749),X749) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_53])])])])])])]) ).
cnf(c_0_59,plain,
( ~ ron(X2,X1)
| ~ rpoint(X2)
| ~ rcenter(vd1089,X1)
| ~ rless(vf(vd1089,vd1080),vf(vd1089,X2))
| rinside(vd1085,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_54]),c_0_55])]) ).
cnf(c_0_60,plain,
( ~ ron(X2,vskolem1102)
| ~ rpoint(X2)
| ~ rcenter(X1,vskolem1102)
| rless(vf(X1,vd1080),vf(X1,X2)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37,c_0_56]),c_0_33])]) ).
cnf(c_0_61,negated_conjecture,
( ~ rpoint(X1)
| ~ ron(X1,vd1101)
| ~ ron(X1,vd1098)
| ~ rR(vd1085,X1,vd1089) ),
inference(split_conjunct,[status(thm)],[c_0_57]) ).
cnf(c_0_62,plain,
vd1098 = vskolem1099,
inference(split_conjunct,[status(thm)],['replace(pred(230, 2))']) ).
cnf(c_0_63,plain,
vd1101 = vskolem1102,
inference(split_conjunct,[status(thm)],['replace(pred(231, 2))']) ).
cnf(c_0_64,plain,
( ~ rcircle(X3)
| X2 != X3
| ~ rline(X5)
| X4 != X5
| ~ rpoint(X6)
| X1 != X6
| ~ rinside(X1,X2)
| ~ ron(X1,X4)
| ~ rpoint(X8)
| X7 != X8
| ~ ron(X7,X4)
| X7 = X1
| rR(X1,esk1_7(X2,X3,X4,X5,X1,X6,X7),X7) ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
cnf(c_0_65,plain,
( ~ ron(X2,X1)
| ~ ron(X2,vskolem1102)
| ~ rpoint(X2)
| ~ rcenter(vd1089,X1)
| rinside(vd1085,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59,c_0_60]),c_0_41])]) ).
cnf(c_0_66,negated_conjecture,
( ~ rR(vd1085,X1,vd1089)
| ~ ron(X1,vskolem1102)
| ~ ron(X1,vskolem1099)
| ~ rpoint(X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_61,c_0_62]),c_0_63]) ).
cnf(c_0_67,plain,
( ~ ron(X1,X4)
| ~ ron(X2,X4)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rcircle(X3)
| ~ rinside(X1,X3)
| ~ rline(X4)
| rR(X1,esk1_7(X3,X3,X4,X4,X1,X1,X2),X2)
| X1 = X2 ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_64])])])]) ).
cnf(c_0_68,plain,
( ~ rcircle(X2)
| X1 != X2
| ~ rline(X4)
| X3 != X4
| ~ rpoint(X6)
| X5 != X6
| ~ rinside(X5,X1)
| ~ ron(X5,X3)
| ~ rpoint(X8)
| X7 != X8
| ~ ron(X7,X3)
| X7 = X5
| ron(esk1_7(X1,X2,X3,X4,X5,X6,X7),X1) ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
cnf(c_0_69,plain,
( ~ ron(X1,vskolem1102)
| ~ rpoint(X1)
| rinside(vd1085,vskolem1102) ),
inference(spm,[status(thm)],[c_0_65,c_0_41]) ).
cnf(c_0_70,negated_conjecture,
( ~ ron(vd1085,X1)
| ~ ron(vd1089,X1)
| ~ ron(esk1_7(X2,X2,X1,X1,vd1085,vd1085,vd1089),vskolem1102)
| ~ ron(esk1_7(X2,X2,X1,X1,vd1085,vd1085,vd1089),vskolem1099)
| ~ rpoint(esk1_7(X2,X2,X1,X1,vd1085,vd1085,vd1089))
| ~ rcircle(X2)
| ~ rinside(vd1085,X2)
| ~ rline(X1)
| vd1085 = vd1089 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66,c_0_67]),c_0_31]),c_0_55])]) ).
cnf(c_0_71,plain,
( ~ ron(X1,X4)
| ~ ron(X2,X4)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rcircle(X3)
| ~ rinside(X1,X3)
| ~ rline(X4)
| ron(esk1_7(X3,X3,X4,X4,X1,X1,X2),X3)
| X1 = X2 ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_68])])])]) ).
cnf(c_0_72,plain,
rcircle(vskolem1102),
inference(split_conjunct,[status(thm)],['replace(replace(and(pred(comma_conjunct2(the(231)), 0), and(pred(comma_conjunct1(the(231)), 0), pred(the(231), 0)))))']) ).
cnf(c_0_73,plain,
rinside(vd1085,vskolem1102),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_45]),c_0_32])]) ).
cnf(c_0_74,plain,
( ~ rcircle(X2)
| X1 != X2
| ~ rline(X4)
| X3 != X4
| ~ rpoint(X6)
| X5 != X6
| ~ rinside(X5,X1)
| ~ ron(X5,X3)
| ~ rpoint(X8)
| X7 != X8
| ~ ron(X7,X3)
| X7 = X5
| ron(esk1_7(X1,X2,X3,X4,X5,X6,X7),X3) ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
fof(c_0_75,plain,
! [X806,X807,X808,X809] :
( ( ~ rpoint(X809)
| X806 != X809
| ~ rpoint(X808)
| X807 != X808
| vf(X806,X807) = v0
| X806 != X807 )
& ( ~ rpoint(X809)
| X806 != X809
| ~ rpoint(X808)
| X807 != X808
| X806 = X807
| vf(X806,X807) != v0 ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(162), 0), imp(cond(axiom(162), 0)))'])])])])]) ).
fof(c_0_76,plain,
vd1085 != vd1080,
inference(fof_simplification,[status(thm)],['holds(conjunct1(225), 1087, 0)']) ).
cnf(c_0_77,negated_conjecture,
( ~ ron(vd1085,X1)
| ~ ron(vd1089,X1)
| ~ ron(esk1_7(vskolem1102,vskolem1102,X1,X1,vd1085,vd1085,vd1089),vskolem1099)
| ~ rpoint(esk1_7(vskolem1102,vskolem1102,X1,X1,vd1085,vd1085,vd1089))
| ~ rline(X1)
| vd1085 = vd1089 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_70,c_0_71]),c_0_72]),c_0_31]),c_0_55])]),c_0_73])]) ).
cnf(c_0_78,plain,
( ~ ron(X1,X4)
| ~ ron(X2,X4)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rcircle(X3)
| ~ rinside(X1,X3)
| ~ rline(X4)
| ron(esk1_7(X3,X3,X4,X4,X1,X1,X2),X4)
| X1 = X2 ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_74])])])]) ).
cnf(c_0_79,plain,
rline(vskolem1099),
inference(split_conjunct,[status(thm)],['replace(replace(and(pred(s2(plural(the(230))), 0), and(pred(s1(plural(the(230))), 0), pred(the(230), 0)))))']) ).
cnf(c_0_80,plain,
ron(vd1089,vskolem1099),
inference(split_conjunct,[status(thm)],['replace(replace(and(pred(s2(plural(the(230))), 0), and(pred(s1(plural(the(230))), 0), pred(the(230), 0)))))']) ).
cnf(c_0_81,plain,
ron(vd1085,vskolem1099),
inference(split_conjunct,[status(thm)],['replace(replace(and(pred(s2(plural(the(230))), 0), and(pred(s1(plural(the(230))), 0), pred(the(230), 0)))))']) ).
cnf(c_0_82,plain,
( ~ rcircle(X2)
| X1 != X2
| ~ rline(X4)
| X3 != X4
| ~ rpoint(X6)
| X5 != X6
| ~ rinside(X5,X1)
| ~ ron(X5,X3)
| ~ rpoint(X8)
| X7 != X8
| ~ ron(X7,X3)
| X7 = X5
| rpoint(esk1_7(X1,X2,X3,X4,X5,X6,X7)) ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
cnf(c_0_83,plain,
( ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| vf(X1,X2) != v0
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_75]) ).
fof(c_0_84,plain,
vd1085 != vd1080,
inference(fof_nnf,[status(thm)],[c_0_76]) ).
cnf(c_0_85,negated_conjecture,
( ~ rpoint(esk1_7(vskolem1102,vskolem1102,vskolem1099,vskolem1099,vd1085,vd1085,vd1089))
| vd1085 = vd1089 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77,c_0_78]),c_0_79]),c_0_80]),c_0_81]),c_0_73]),c_0_72]),c_0_31]),c_0_55])]) ).
cnf(c_0_86,plain,
( ~ ron(X1,X4)
| ~ ron(X2,X4)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rcircle(X3)
| ~ rinside(X1,X3)
| ~ rline(X4)
| rpoint(esk1_7(X3,X3,X4,X4,X1,X1,X2))
| X1 = X2 ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_82])])])]) ).
cnf(c_0_87,plain,
( ~ rpoint(X2)
| ~ rpoint(X1)
| vf(X1,X2) != v0
| X1 = X2 ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_83])]) ).
cnf(c_0_88,plain,
vf(vd1089,vd1080) = vf(vd1085,vd1080),
inference(split_conjunct,[status(thm)],['holds(226, 1090, 1)']) ).
cnf(c_0_89,plain,
vd1085 != vd1080,
inference(split_conjunct,[status(thm)],[c_0_84]) ).
cnf(c_0_90,negated_conjecture,
vd1085 = vd1089,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_85,c_0_86]),c_0_79]),c_0_73]),c_0_72]),c_0_31]),c_0_55]),c_0_80]),c_0_81])]) ).
cnf(c_0_91,plain,
vf(vd1089,vd1080) != v0,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_87,c_0_88]),c_0_55]),c_0_33])]),c_0_89]) ).
cnf(c_0_92,plain,
vf(vd1089,vd1080) = vf(vd1089,vd1089),
inference(rw,[status(thm)],[c_0_54,c_0_90]) ).
cnf(c_0_93,plain,
( ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| X1 != X2
| vf(X1,X2) = v0 ),
inference(split_conjunct,[status(thm)],[c_0_75]) ).
cnf(c_0_94,plain,
vf(vd1089,vd1089) != v0,
inference(rw,[status(thm)],[c_0_91,c_0_92]) ).
cnf(c_0_95,plain,
( ~ rpoint(X1)
| vf(X1,X1) = v0 ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_93])])]) ).
cnf(c_0_96,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94,c_0_95]),c_0_31])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO279+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/10.38 % Computer : n011.cluster.edu
% 0.11/10.38 % Model : x86_64 x86_64
% 0.11/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.38 % Memory : 8046.5625MB
% 0.11/10.38 % OS : Linux 6.8.0-71-generic
% 0.11/10.39 % CPULimit : 300
% 0.11/10.39 % WCLimit : 300
% 0.11/10.39 % DateTime : Sun Sep 20 15:04:35 UTC 2026
% 0.11/10.39 % CPUTime :
% 0.11/10.39 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/10.43 Running first-order theorem proving
% 0.15/10.43 Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 94.01/24.18 % Version: 3.5.1
% 94.01/24.18 % Preprocessing class: FSLSSMSMSSSNFFN.
% 94.01/24.18 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 94.01/24.18 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 94.01/24.18 % Starting new_bool_3 with 300s (1) cores
% 94.01/24.18 % Starting new_bool_1 with 300s (1) cores
% 94.01/24.18 % Starting sh5l with 300s (1) cores
% 94.01/24.18 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 3833649 completed with status 0
% 94.01/24.18 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 94.01/24.18 % Preprocessing class: FSLSSMSMSSSNFFN.
% 94.01/24.18 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 94.01/24.18 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 94.01/24.18 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 94.01/24.18 % No SInE strategy applied
% 94.01/24.18 % Search class: FGHSF-FSLM33-SFFFFFNN
% 94.01/24.18 % Scheduled 11 strats onto 5 cores with 1500 seconds (1500 total)
% 94.01/24.18 % Starting SubtermCWHack with 136s (1) cores
% 94.01/24.18 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 94.01/24.18 % Starting G-E--_302_C18_F1_URBAN_S0Y with 136s (1) cores
% 94.01/24.18 % Starting H----_102_C18_F1_PI_AE_CS_SP_PS_S0Y with 136s (1) cores
% 94.01/24.18 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 136s (1) cores
% 94.01/24.18 % G-E--_302_C18_F1_URBAN_S0Y with pid 3833657 completed with status 0
% 94.01/24.18 % Result found by G-E--_302_C18_F1_URBAN_S0Y
% 94.01/24.18 % Preprocessing class: FSLSSMSMSSSNFFN.
% 94.01/24.18 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 94.01/24.18 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 94.01/24.18 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 94.01/24.18 % No SInE strategy applied
% 94.01/24.18 % Search class: FGHSF-FSLM33-SFFFFFNN
% 94.01/24.18 % Scheduled 11 strats onto 5 cores with 1500 seconds (1500 total)
% 94.01/24.18 % Starting SubtermCWHack with 136s (1) cores
% 94.01/24.18 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 94.01/24.18 % Starting G-E--_302_C18_F1_URBAN_S0Y with 136s (1) cores
% 94.01/24.18 % Preprocessing time : 0.018 s
% 94.01/24.18
% 94.01/24.18 % Proof found!
% 94.01/24.18 % SZS status Theorem
% 94.01/24.18 % SZS output start CNFRefutation
% See solution above
% 94.01/24.18 % Parsed axioms : 132
% 94.01/24.18 % Removed by relevancy pruning/SinE : 0
% 94.01/24.18 % Initial clauses : 288
% 94.01/24.18 % Removed in clause preprocessing : 2
% 94.01/24.18 % Initial clauses in saturation : 286
% 94.01/24.18 % Processed clauses : 9388
% 94.01/24.18 % ...of these trivial : 175
% 94.01/24.18 % ...subsumed : 4425
% 94.01/24.18 % ...remaining for further processing : 4788
% 94.01/24.18 % Other redundant clauses eliminated : 1094
% 94.01/24.18 % Clauses deleted for lack of memory : 0
% 94.01/24.18 % Backward-subsumed : 585
% 94.01/24.18 % Backward-rewritten : 2345
% 94.01/24.18 % Generated clauses : 149722
% 94.01/24.18 % ...of the previous two non-redundant : 134358
% 94.01/24.18 % ...aggressively subsumed : 0
% 94.01/24.18 % Contextual simplify-reflections : 976
% 94.01/24.18 % Paramodulations : 149442
% 94.01/24.18 % Factorizations : 0
% 94.01/24.18 % NegExts : 0
% 94.01/24.18 % Equation resolutions : 1134
% 94.01/24.18 % Disequality decompositions : 0
% 94.01/24.18 % Total rewrite steps : 170475
% 94.01/24.18 % ...of those cached : 170424
% 94.01/24.18 % Propositional unsat checks : 0
% 94.01/24.18 % Propositional check models : 0
% 94.01/24.18 % Propositional check unsatisfiable : 0
% 94.01/24.18 % Propositional clauses : 0
% 94.01/24.18 % Propositional clauses after purity: 0
% 94.01/24.18 % Propositional unsat core size : 0
% 94.01/24.18 % Propositional preprocessing time : 0.000
% 94.01/24.18 % Propositional encoding time : 0.000
% 94.01/24.18 % Propositional solver time : 0.000
% 94.01/24.18 % Success case prop preproc time : 0.000
% 94.01/24.18 % Success case prop encoding time : 0.000
% 94.01/24.18 % Success case prop solver time : 0.000
% 94.01/24.18 % Current number of processed clauses : 1618
% 94.01/24.18 % Positive orientable unit clauses : 37
% 94.01/24.18 % Positive unorientable unit clauses: 0
% 94.01/24.18 % Negative unit clauses : 17
% 94.01/24.18 % Non-unit-clauses : 1564
% 94.01/24.18 % Current number of unprocessed clauses: 124039
% 94.01/24.18 % ...number of literals in the above : 2007274
% 94.01/24.18 % Current number of archived formulas : 0
% 94.01/24.18 % Current number of archived clauses : 2935
% 94.01/24.18 % Clause-clause subsumption calls (NU) : 6871135
% 94.01/24.18 % Rec. Clause-clause subsumption calls : 93302
% 94.01/24.18 % Non-unit clause-clause subsumptions : 4663
% 94.01/24.18 % Unit Clause-clause subsumption calls : 14322
% 94.01/24.18 % Rewrite failures with RHS unbound : 0
% 94.01/24.18 % BW rewrite match attempts : 10
% 94.01/24.18 % BW rewrite match successes : 10
% 94.01/24.18 % Condensation attempts : 0
% 94.01/24.18 % Condensation successes : 0
% 94.01/24.18 % Termbank termtop insertions : 7246540
% 94.01/24.18 % Search garbage collected termcells : 13961
% 94.01/24.18
% 94.01/24.18 % -------------------------------------------------
% 94.01/24.18 % User time : 13.177 s
% 94.01/24.18 % System time : 0.223 s
% 94.01/24.18 % Total time : 13.400 s
% 94.01/24.18 % Maximum resident set size: 6008 pages
% 94.01/24.18
% 94.01/24.18 % -------------------------------------------------
% 94.01/24.18 % User time : 65.627 s
% 94.01/24.18 % System time : 1.372 s
% 94.01/24.18 % Total time : 66.999 s
% 94.01/24.18 % Maximum resident set size: 5632 pages
% 94.01/24.18 % E exiting
%------------------------------------------------------------------------------