%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO270+1 : TPTP v9.2.1. Released v4.1.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 : n011.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:20:12 PM UTC 2026
% Result : Theorem 1.78s 1.89s
% Output : CNFRefutation 1.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 5
% Syntax : Number of formulae : 28 ( 9 unt; 0 def)
% Number of atoms : 117 ( 74 equ)
% Maximal formula atoms : 8 ( 4 avg)
% Number of connectives : 150 ( 61 ~; 60 |; 20 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-6 aty)
% Number of variables : 65 ( 0 sgn 37 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof('qe(208)',conjecture,
? [X1] :
( vf(vd1049,X1) = vf(X1,vd1047)
& vf(vd1047,vd1049) = vf(vd1049,X1)
& rpoint(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(208)') ).
fof('ass(cond(proof(209), 0), 1)',axiom,
! [X2,X3,X4,X5] :
( ( X4 = X5
& X2 != X4
& rpoint(X5)
& X2 = X3
& rpoint(X3) )
=> ! [X6] :
( X6 = vskolem1061(X2,X3,X4,X5)
=> ! [X7] :
( X7 = vskolem1063(X6,X2,X3,X4,X5)
=> vf(X2,X4) = vf(X4,vskolem1064(X7,X6,X2,X3,X4,X5)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(proof(209), 0), 1)') ).
fof('and(pred(conjunct2(207), 4), and(holds(conjunct2(207), 1051, 0), and(pred(conjunct2(207), 1), and(pred(conjunct1(207), 2), pred(conjunct1(207), 1)))))',axiom,
( vd1049 = vd1050
& vd1047 != vd1049
& rpoint(vd1050)
& vd1047 = vd1048
& rpoint(vd1048) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','and(pred(conjunct2(207), 4), and(holds(conjunct2(207), 1051, 0), and(pred(conjunct2(207), 1), and(pred(conjunct1(207), 2), pred(conjunct1(207), 1)))))') ).
fof('ass(cond(proof(209), 0), 0)',axiom,
! [X2,X3,X4,X5] :
( ( X4 = X5
& X2 != X4
& rpoint(X5)
& X2 = X3
& rpoint(X3) )
=> ! [X6] :
( X6 = vskolem1061(X2,X3,X4,X5)
=> ! [X7] :
( X7 = vskolem1063(X6,X2,X3,X4,X5)
=> vf(X4,vskolem1064(X7,X6,X2,X3,X4,X5)) = vf(vskolem1064(X7,X6,X2,X3,X4,X5),X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(proof(209), 0), 0)') ).
fof('ass(cond(proof(209), 0), 6)',axiom,
! [X2,X3,X4,X5] :
( ( X4 = X5
& X2 != X4
& rpoint(X5)
& X2 = X3
& rpoint(X3) )
=> ! [X6] :
( X6 = vskolem1061(X2,X3,X4,X5)
=> ! [X7] :
( X7 = vskolem1063(X6,X2,X3,X4,X5)
=> rpoint(vskolem1064(X7,X6,X2,X3,X4,X5)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(proof(209), 0), 6)') ).
fof(c_0_5,negated_conjecture,
~ ? [X1] :
( vf(vd1049,X1) = vf(X1,vd1047)
& vf(vd1047,vd1049) = vf(vd1049,X1)
& rpoint(X1) ),
inference(assume_negation,[status(cth)],['qe(208)']) ).
fof(c_0_6,plain,
! [X1537,X1538,X1539,X1540,X1541,X1542] :
( X1539 != X1540
| X1537 = X1539
| ~ rpoint(X1540)
| X1537 != X1538
| ~ rpoint(X1538)
| X1541 != vskolem1061(X1537,X1538,X1539,X1540)
| X1542 != vskolem1063(X1541,X1537,X1538,X1539,X1540)
| vf(X1537,X1539) = vf(X1539,vskolem1064(X1542,X1541,X1537,X1538,X1539,X1540)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(proof(209), 0), 1)'])])]) ).
fof(c_0_7,negated_conjecture,
! [X1530] :
( vf(vd1049,X1530) != vf(X1530,vd1047)
| vf(vd1047,vd1049) != vf(vd1049,X1530)
| ~ rpoint(X1530) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])]) ).
cnf(c_0_8,plain,
( X3 = X1
| vf(X3,X1) = vf(X1,vskolem1064(X6,X5,X3,X4,X1,X2))
| X1 != X2
| ~ rpoint(X2)
| X3 != X4
| ~ rpoint(X4)
| X5 != vskolem1061(X3,X4,X1,X2)
| X6 != vskolem1063(X5,X3,X4,X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_9,plain,
rpoint(vd1050),
inference(split_conjunct,[status(thm)],['and(pred(conjunct2(207), 4), and(holds(conjunct2(207), 1051, 0), and(pred(conjunct2(207), 1), and(pred(conjunct1(207), 2), pred(conjunct1(207), 1)))))']) ).
cnf(c_0_10,plain,
vd1049 = vd1050,
inference(split_conjunct,[status(thm)],['and(pred(conjunct2(207), 4), and(holds(conjunct2(207), 1051, 0), and(pred(conjunct2(207), 1), and(pred(conjunct1(207), 2), pred(conjunct1(207), 1)))))']) ).
fof(c_0_11,plain,
! [X1531,X1532,X1533,X1534,X1535,X1536] :
( X1533 != X1534
| X1531 = X1533
| ~ rpoint(X1534)
| X1531 != X1532
| ~ rpoint(X1532)
| X1535 != vskolem1061(X1531,X1532,X1533,X1534)
| X1536 != vskolem1063(X1535,X1531,X1532,X1533,X1534)
| vf(X1533,vskolem1064(X1536,X1535,X1531,X1532,X1533,X1534)) = vf(vskolem1064(X1536,X1535,X1531,X1532,X1533,X1534),X1531) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(proof(209), 0), 0)'])])]) ).
cnf(c_0_12,negated_conjecture,
( vf(vd1049,X1) != vf(X1,vd1047)
| vf(vd1047,vd1049) != vf(vd1049,X1)
| ~ rpoint(X1) ),
inference(split_conjunct,[status(thm)],[c_0_7]) ).
cnf(c_0_13,plain,
( vf(X1,vskolem1064(vskolem1063(vskolem1061(X2,X2,X1,X1),X2,X2,X1,X1),vskolem1061(X2,X2,X1,X1),X2,X2,X1,X1)) = vf(X2,X1)
| X1 = X2
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_8])])])]) ).
cnf(c_0_14,plain,
rpoint(vd1049),
inference(rw,[status(thm)],[c_0_9,c_0_10]) ).
cnf(c_0_15,plain,
( X3 = X1
| vf(X1,vskolem1064(X6,X5,X3,X4,X1,X2)) = vf(vskolem1064(X6,X5,X3,X4,X1,X2),X3)
| X1 != X2
| ~ rpoint(X2)
| X3 != X4
| ~ rpoint(X4)
| X5 != vskolem1061(X3,X4,X1,X2)
| X6 != vskolem1063(X5,X3,X4,X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
cnf(c_0_16,plain,
rpoint(vd1048),
inference(split_conjunct,[status(thm)],['and(pred(conjunct2(207), 4), and(holds(conjunct2(207), 1051, 0), and(pred(conjunct2(207), 1), and(pred(conjunct1(207), 2), pred(conjunct1(207), 1)))))']) ).
cnf(c_0_17,plain,
vd1047 = vd1048,
inference(split_conjunct,[status(thm)],['and(pred(conjunct2(207), 4), and(holds(conjunct2(207), 1051, 0), and(pred(conjunct2(207), 1), and(pred(conjunct1(207), 2), pred(conjunct1(207), 1)))))']) ).
cnf(c_0_18,negated_conjecture,
( vd1049 = X1
| vf(vskolem1064(vskolem1063(vskolem1061(X1,X1,vd1049,vd1049),X1,X1,vd1049,vd1049),vskolem1061(X1,X1,vd1049,vd1049),X1,X1,vd1049,vd1049),vd1047) != vf(X1,vd1049)
| vf(vd1047,vd1049) != vf(X1,vd1049)
| ~ rpoint(vskolem1064(vskolem1063(vskolem1061(X1,X1,vd1049,vd1049),X1,X1,vd1049,vd1049),vskolem1061(X1,X1,vd1049,vd1049),X1,X1,vd1049,vd1049))
| ~ rpoint(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12,c_0_13]),c_0_14])]) ).
cnf(c_0_19,plain,
( vf(X1,vskolem1064(vskolem1063(vskolem1061(X2,X2,X1,X1),X2,X2,X1,X1),vskolem1061(X2,X2,X1,X1),X2,X2,X1,X1)) = vf(vskolem1064(vskolem1063(vskolem1061(X2,X2,X1,X1),X2,X2,X1,X1),vskolem1061(X2,X2,X1,X1),X2,X2,X1,X1),X2)
| X1 = X2
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_15])])])]) ).
cnf(c_0_20,plain,
rpoint(vd1047),
inference(rw,[status(thm)],[c_0_16,c_0_17]) ).
cnf(c_0_21,plain,
vd1047 != vd1049,
inference(split_conjunct,[status(thm)],['and(pred(conjunct2(207), 4), and(holds(conjunct2(207), 1051, 0), and(pred(conjunct2(207), 1), and(pred(conjunct1(207), 2), pred(conjunct1(207), 1)))))']) ).
fof(c_0_22,plain,
! [X1567,X1568,X1569,X1570,X1571,X1572] :
( X1569 != X1570
| X1567 = X1569
| ~ rpoint(X1570)
| X1567 != X1568
| ~ rpoint(X1568)
| X1571 != vskolem1061(X1567,X1568,X1569,X1570)
| X1572 != vskolem1063(X1571,X1567,X1568,X1569,X1570)
| rpoint(vskolem1064(X1572,X1571,X1567,X1568,X1569,X1570)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(proof(209), 0), 6)'])])]) ).
cnf(c_0_23,negated_conjecture,
( vf(vd1049,vskolem1064(vskolem1063(vskolem1061(vd1047,vd1047,vd1049,vd1049),vd1047,vd1047,vd1049,vd1049),vskolem1061(vd1047,vd1047,vd1049,vd1049),vd1047,vd1047,vd1049,vd1049)) != vf(vd1047,vd1049)
| ~ rpoint(vskolem1064(vskolem1063(vskolem1061(vd1047,vd1047,vd1049,vd1049),vd1047,vd1047,vd1049,vd1049),vskolem1061(vd1047,vd1047,vd1049,vd1049),vd1047,vd1047,vd1049,vd1049)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_18,c_0_19]),c_0_20]),c_0_14])]),c_0_21]) ).
cnf(c_0_24,plain,
( X3 = X1
| rpoint(vskolem1064(X6,X5,X3,X4,X1,X2))
| X1 != X2
| ~ rpoint(X2)
| X3 != X4
| ~ rpoint(X4)
| X5 != vskolem1061(X3,X4,X1,X2)
| X6 != vskolem1063(X5,X3,X4,X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_25,negated_conjecture,
~ rpoint(vskolem1064(vskolem1063(vskolem1061(vd1047,vd1047,vd1049,vd1049),vd1047,vd1047,vd1049,vd1049),vskolem1061(vd1047,vd1047,vd1049,vd1049),vd1047,vd1047,vd1049,vd1049)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23,c_0_13]),c_0_20]),c_0_14])]),c_0_21]) ).
cnf(c_0_26,plain,
( X1 = X2
| rpoint(vskolem1064(vskolem1063(vskolem1061(X2,X2,X1,X1),X2,X2,X1,X1),vskolem1061(X2,X2,X1,X1),X2,X2,X1,X1))
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_24])])])]) ).
cnf(c_0_27,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25,c_0_26]),c_0_20]),c_0_14])]),c_0_21]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO270+1 : TPTP v9.2.1. Released v4.1.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.33 % Computer : n011.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 17:51:17 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 1.78/1.89 % Version : CSE_E---1.7
% 1.78/1.89 % Problem : theBenchmark.p
% 1.78/1.89 % SZS status Theorem for theBenchmark.p
% 1.78/1.89 % SZS output start CNFRefutation
% See solution above
% 1.78/1.89 % Total time : 1.424s
%------------------------------------------------------------------------------