%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO528+1 : TPTP v9.2.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n026.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 : Tue May 5 04:21:27 PM UTC 2026
% Result : Theorem 6.43s 4.53s
% Output : CNFRefutation 6.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 11
% Syntax : Number of formulae : 56 ( 14 unt; 0 def)
% Number of atoms : 204 ( 52 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 241 ( 93 ~; 123 |; 25 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-4 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-4 aty)
% Number of variables : 152 ( 0 sgn 96 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(aSatz8_18a,axiom,
! [X12,X15,X14,X13,X16] :
( s_col(X12,X15,X14)
| ~ s_col(X12,X15,X13)
| ~ s_col(X12,X15,X16)
| ~ perp(X12,X15,X14,X13)
| ~ perp(X12,X15,X14,X16)
| X13 = X16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz8_18a) ).
fof(aSatz8_14a,axiom,
! [X12,X15,X13,X16] :
( ~ perp(X12,X15,X13,X16)
| ~ s_col(X12,X15,X13)
| ~ s_col(X12,X15,X16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz8_14a) ).
fof(aSatz10_14,conjecture,
! [X12,X15,X13,X37] :
( X12 = X15
| reflect(X12,X15,X13) != X37
| s_col(X12,X15,X13)
| opposite(X13,X12,X15,X37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz10_14) ).
fof(aSatz10_8a,axiom,
! [X12,X15,X13] :
( X12 = X15
| reflect(X12,X15,X13) != X13
| s_col(X12,X15,X13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz10_8a) ).
fof(aSatz10_8b,axiom,
! [X12,X15,X13] :
( X12 = X15
| ~ s_col(X12,X15,X13)
| reflect(X12,X15,X13) = X13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz10_8b) ).
fof(aSatz8_18,axiom,
! [X12,X15,X14] :
( ( s_col(X12,X15,X14)
| s_col(X12,X15,foot(X12,X15,X14)) )
& ( s_col(X12,X15,X14)
| perp(X12,X15,X14,foot(X12,X15,X14)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz8_18) ).
fof(aSatz10_2a,axiom,
! [X12,X15,X13] :
( ( X12 = X15
| s_col(X12,X15,midpoint(X13,reflect(X12,X15,X13))) )
& ( X12 = X15
| X13 = reflect(X12,X15,X13)
| perp(X12,X15,X13,reflect(X12,X15,X13)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz10_2a) ).
fof(d_Defn9_1,axiom,
! [X13,X16,X12,X15,X36] :
( ( X13 = X16
| s_col(X13,X16,X12)
| s_col(X13,X16,X15)
| ~ s_t(X12,X36,X15)
| ~ s_col(X13,X16,X36)
| opposite(X12,X13,X16,X15) )
& ( ~ opposite(X12,X13,X16,X15)
| ~ s_col(X13,X16,X12) )
& ( ~ opposite(X12,X13,X16,X15)
| ~ s_col(X13,X16,X15) )
& ( ~ opposite(X12,X13,X16,X15)
| s_t(X12,il(X12,X15,X13,X16),X15) )
& ( ~ opposite(X12,X13,X16,X15)
| s_col(X13,X16,il(X12,X15,X13,X16)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_Defn9_1) ).
fof(d_Defn7_1,axiom,
! [X12,X29,X15] :
( ( ~ s_m(X12,X29,X15)
| s_t(X12,X29,X15) )
& ( ~ s_m(X12,X29,X15)
| s_e(X29,X12,X29,X15) )
& ( ~ s_t(X12,X29,X15)
| ~ s_e(X29,X12,X29,X15)
| s_m(X12,X29,X15) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_Defn7_1) ).
fof(aSatz10_5,axiom,
! [X12,X15,X13] :
( X12 = X15
| reflect(X12,X15,reflect(X12,X15,X13)) = X13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz10_5) ).
fof(aSatz8_22,axiom,
! [X12,X15] : s_m(X12,midpoint(X12,X15),X15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz8_22) ).
fof(c_0_11,plain,
! [X12,X15,X14,X13,X16] :
( s_col(X12,X15,X14)
| ~ s_col(X12,X15,X13)
| ~ s_col(X12,X15,X16)
| ~ perp(X12,X15,X14,X13)
| ~ perp(X12,X15,X14,X16)
| X13 = X16 ),
inference(fof_simplification,[status(thm)],[aSatz8_18a]) ).
fof(c_0_12,plain,
! [X12,X15,X13,X16] :
( ~ perp(X12,X15,X13,X16)
| ~ s_col(X12,X15,X13)
| ~ s_col(X12,X15,X16) ),
inference(fof_simplification,[status(thm)],[aSatz8_14a]) ).
fof(c_0_13,negated_conjecture,
~ ! [X12,X15,X13,X37] :
( X12 = X15
| reflect(X12,X15,X13) != X37
| s_col(X12,X15,X13)
| opposite(X13,X12,X15,X37) ),
inference(assume_negation,[status(cth)],[aSatz10_14]) ).
fof(c_0_14,plain,
! [X1469,X1470,X1471,X1472,X1473] :
( s_col(X1469,X1470,X1471)
| ~ s_col(X1469,X1470,X1472)
| ~ s_col(X1469,X1470,X1473)
| ~ perp(X1469,X1470,X1471,X1472)
| ~ perp(X1469,X1470,X1471,X1473)
| X1472 = X1473 ),
inference(variable_rename,[status(thm)],[c_0_11]) ).
fof(c_0_15,plain,
! [X1441,X1442,X1443,X1444] :
( ~ perp(X1441,X1442,X1443,X1444)
| ~ s_col(X1441,X1442,X1443)
| ~ s_col(X1441,X1442,X1444) ),
inference(variable_rename,[status(thm)],[c_0_12]) ).
fof(c_0_16,plain,
! [X1727,X1728,X1729] :
( X1727 = X1728
| reflect(X1727,X1728,X1729) != X1729
| s_col(X1727,X1728,X1729) ),
inference(variable_rename,[status(thm)],[aSatz10_8a]) ).
fof(c_0_17,negated_conjecture,
( esk1_0 != esk2_0
& reflect(esk1_0,esk2_0,esk3_0) = esk4_0
& ~ s_col(esk1_0,esk2_0,esk3_0)
& ~ opposite(esk3_0,esk1_0,esk2_0,esk4_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_13])])]) ).
fof(c_0_18,plain,
! [X12,X15,X13] :
( X12 = X15
| ~ s_col(X12,X15,X13)
| reflect(X12,X15,X13) = X13 ),
inference(fof_simplification,[status(thm)],[aSatz10_8b]) ).
cnf(c_0_19,plain,
( s_col(X1,X2,X3)
| X4 = X5
| ~ s_col(X1,X2,X4)
| ~ s_col(X1,X2,X5)
| ~ perp(X1,X2,X3,X4)
| ~ perp(X1,X2,X3,X5) ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
cnf(c_0_20,plain,
( ~ perp(X1,X2,X3,X4)
| ~ s_col(X1,X2,X3)
| ~ s_col(X1,X2,X4) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
fof(c_0_21,plain,
! [X1474,X1475,X1476] :
( ( s_col(X1474,X1475,X1476)
| s_col(X1474,X1475,foot(X1474,X1475,X1476)) )
& ( s_col(X1474,X1475,X1476)
| perp(X1474,X1475,X1476,foot(X1474,X1475,X1476)) ) ),
inference(variable_rename,[status(thm)],[aSatz8_18]) ).
fof(c_0_22,plain,
! [X1705,X1706,X1707] :
( ( X1705 = X1706
| s_col(X1705,X1706,midpoint(X1707,reflect(X1705,X1706,X1707))) )
& ( X1705 = X1706
| X1707 = reflect(X1705,X1706,X1707)
| perp(X1705,X1706,X1707,reflect(X1705,X1706,X1707)) ) ),
inference(variable_rename,[status(thm)],[aSatz10_2a]) ).
cnf(c_0_23,plain,
( X1 = X2
| s_col(X1,X2,X3)
| reflect(X1,X2,X3) != X3 ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_24,negated_conjecture,
reflect(esk1_0,esk2_0,esk3_0) = esk4_0,
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_25,negated_conjecture,
esk1_0 != esk2_0,
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_26,negated_conjecture,
~ s_col(esk1_0,esk2_0,esk3_0),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
fof(c_0_27,plain,
! [X13,X16,X12,X15,X36] :
( ( X13 = X16
| s_col(X13,X16,X12)
| s_col(X13,X16,X15)
| ~ s_t(X12,X36,X15)
| ~ s_col(X13,X16,X36)
| opposite(X12,X13,X16,X15) )
& ( ~ opposite(X12,X13,X16,X15)
| ~ s_col(X13,X16,X12) )
& ( ~ opposite(X12,X13,X16,X15)
| ~ s_col(X13,X16,X15) )
& ( ~ opposite(X12,X13,X16,X15)
| s_t(X12,il(X12,X15,X13,X16),X15) )
& ( ~ opposite(X12,X13,X16,X15)
| s_col(X13,X16,il(X12,X15,X13,X16)) ) ),
inference(fof_simplification,[status(thm)],[d_Defn9_1]) ).
fof(c_0_28,plain,
! [X12,X29,X15] :
( ( ~ s_m(X12,X29,X15)
| s_t(X12,X29,X15) )
& ( ~ s_m(X12,X29,X15)
| s_e(X29,X12,X29,X15) )
& ( ~ s_t(X12,X29,X15)
| ~ s_e(X29,X12,X29,X15)
| s_m(X12,X29,X15) ) ),
inference(fof_simplification,[status(thm)],[d_Defn7_1]) ).
fof(c_0_29,plain,
! [X1730,X1731,X1732] :
( X1730 = X1731
| ~ s_col(X1730,X1731,X1732)
| reflect(X1730,X1731,X1732) = X1732 ),
inference(variable_rename,[status(thm)],[c_0_18]) ).
cnf(c_0_30,plain,
( X1 = X2
| ~ perp(X3,X4,X5,X2)
| ~ perp(X3,X4,X5,X1)
| ~ s_col(X3,X4,X2)
| ~ s_col(X3,X4,X1) ),
inference(csr,[status(thm)],[c_0_19,c_0_20]) ).
cnf(c_0_31,plain,
( s_col(X1,X2,X3)
| perp(X1,X2,X3,foot(X1,X2,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_32,plain,
( s_col(X1,X2,X3)
| s_col(X1,X2,foot(X1,X2,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_33,plain,
( X1 = X2
| X3 = reflect(X1,X2,X3)
| perp(X1,X2,X3,reflect(X1,X2,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_34,negated_conjecture,
esk4_0 != esk3_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_23,c_0_24]),c_0_25]),c_0_26]) ).
fof(c_0_35,plain,
! [X1716,X1717,X1718] :
( X1716 = X1717
| reflect(X1716,X1717,reflect(X1716,X1717,X1718)) = X1718 ),
inference(variable_rename,[status(thm)],[aSatz10_5]) ).
fof(c_0_36,plain,
! [X1835,X1836,X1837,X1838,X1839] :
( ( X1835 = X1836
| s_col(X1835,X1836,X1837)
| s_col(X1835,X1836,X1838)
| ~ s_t(X1837,X1839,X1838)
| ~ s_col(X1835,X1836,X1839)
| opposite(X1837,X1835,X1836,X1838) )
& ( ~ opposite(X1837,X1835,X1836,X1838)
| ~ s_col(X1835,X1836,X1837) )
& ( ~ opposite(X1837,X1835,X1836,X1838)
| ~ s_col(X1835,X1836,X1838) )
& ( ~ opposite(X1837,X1835,X1836,X1838)
| s_t(X1837,il(X1837,X1838,X1835,X1836),X1838) )
& ( ~ opposite(X1837,X1835,X1836,X1838)
| s_col(X1835,X1836,il(X1837,X1838,X1835,X1836)) ) ),
inference(variable_rename,[status(thm)],[c_0_27]) ).
cnf(c_0_37,plain,
( X1 = X2
| s_col(X1,X2,midpoint(X3,reflect(X1,X2,X3))) ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
fof(c_0_38,plain,
! [X1810,X1811,X1812] :
( ( ~ s_m(X1810,X1811,X1812)
| s_t(X1810,X1811,X1812) )
& ( ~ s_m(X1810,X1811,X1812)
| s_e(X1811,X1810,X1811,X1812) )
& ( ~ s_t(X1810,X1811,X1812)
| ~ s_e(X1811,X1810,X1811,X1812)
| s_m(X1810,X1811,X1812) ) ),
inference(variable_rename,[status(thm)],[c_0_28]) ).
fof(c_0_39,plain,
! [X1505,X1506] : s_m(X1505,midpoint(X1505,X1506),X1506),
inference(variable_rename,[status(thm)],[aSatz8_22]) ).
cnf(c_0_40,plain,
( X1 = X2
| reflect(X1,X2,X3) = X3
| ~ s_col(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
cnf(c_0_41,plain,
( X1 = foot(X2,X3,X4)
| ~ perp(X2,X3,X4,X1)
| ~ s_col(X2,X3,X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_30,c_0_31]),c_0_32]),c_0_20]) ).
cnf(c_0_42,negated_conjecture,
perp(esk1_0,esk2_0,esk3_0,esk4_0),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_33,c_0_24]),c_0_25]),c_0_34]) ).
cnf(c_0_43,plain,
( X1 = X2
| reflect(X1,X2,reflect(X1,X2,X3)) = X3 ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
cnf(c_0_44,plain,
( X1 = X2
| s_col(X1,X2,X3)
| s_col(X1,X2,X4)
| opposite(X3,X1,X2,X4)
| ~ s_t(X3,X5,X4)
| ~ s_col(X1,X2,X5) ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
cnf(c_0_45,negated_conjecture,
s_col(esk1_0,esk2_0,midpoint(esk3_0,esk4_0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_37,c_0_24]),c_0_25]) ).
cnf(c_0_46,plain,
( s_t(X1,X2,X3)
| ~ s_m(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_47,plain,
s_m(X1,midpoint(X1,X2),X2),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_48,plain,
( reflect(X1,X2,foot(X1,X2,X3)) = foot(X1,X2,X3)
| X1 = X2
| s_col(X1,X2,X3) ),
inference(spm,[status(thm)],[c_0_40,c_0_32]) ).
cnf(c_0_49,negated_conjecture,
( foot(esk1_0,esk2_0,esk3_0) = esk4_0
| ~ s_col(esk1_0,esk2_0,esk4_0) ),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
cnf(c_0_50,negated_conjecture,
reflect(esk1_0,esk2_0,esk4_0) = esk3_0,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43,c_0_24]),c_0_25]) ).
cnf(c_0_51,negated_conjecture,
( opposite(X1,esk1_0,esk2_0,X2)
| s_col(esk1_0,esk2_0,X1)
| s_col(esk1_0,esk2_0,X2)
| ~ s_t(X1,midpoint(esk3_0,esk4_0),X2) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_44,c_0_45]),c_0_25]) ).
cnf(c_0_52,plain,
s_t(X1,midpoint(X1,X2),X2),
inference(spm,[status(thm)],[c_0_46,c_0_47]) ).
cnf(c_0_53,negated_conjecture,
~ opposite(esk3_0,esk1_0,esk2_0,esk4_0),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_54,negated_conjecture,
~ s_col(esk1_0,esk2_0,esk4_0),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_49]),c_0_50]),c_0_34]),c_0_25]),c_0_26]) ).
cnf(c_0_55,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_52]),c_0_53]),c_0_26]),c_0_54]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO528+1 : TPTP v9.2.1. Released v7.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.32 % Computer : n026.cluster.edu
% 0.16/0.32 % Model : x86_64 x86_64
% 0.16/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.32 % Memory : 8042.1875MB
% 0.16/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.32 % CPULimit : 300
% 0.16/0.32 % WCLimit : 300
% 0.16/0.32 % DateTime : Mon May 4 18:01:53 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 6.43/4.53 % Version : CSE_E---1.7
% 6.43/4.53 % Problem : theBenchmark.p
% 6.43/4.53 % SZS status Theorem for theBenchmark.p
% 6.43/4.53 % SZS output start CNFRefutation
% See solution above
% 6.43/4.56 % Total time : 3.429s
%------------------------------------------------------------------------------