%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO082+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n016.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 : Fri Sep 25 01:16:59 PM UTC 2026
% Result : Theorem 49.86s 7.00s
% Output : Proof 49.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 3
% Syntax : Number of formulae : 26 ( 5 unt; 0 def)
% Number of atoms : 72 ( 19 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 68 ( 22 ~; 26 |; 14 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 34 ( 0 sgn 20 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f15,axiom,
! [C,C1] :
( ! [P] :
( incident_c(P,C)
<=> incident_c(P,C1) )
=> C = C1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c9) ).
fof(f15_nnf,plain,
! [C,C1] :
( C = C1
| ? [P] :
( ( incident_c(P,C1)
& ~ incident_c(P,C) )
| ( ~ incident_c(P,C1)
& incident_c(P,C) ) ) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [C,C1] :
( C = C1
| ( incident_c(sk12(C,C1),C1)
& ~ incident_c(sk12(C,C1),C) )
| ( ~ incident_c(sk12(C,C1),C1)
& incident_c(sk12(C,C1),C) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk12])],[f15_nnf]) ).
cnf(c45,plain,
( X0 = X1
| incident_c(sk12(X0,X1),X1)
| incident_c(sk12(X0,X1),X0) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
fof(f0,axiom,
! [C,C1] :
( part_of(C1,C)
<=> ! [P] :
( incident_c(P,C1)
=> incident_c(P,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',part_of_defn) ).
fof(f0_nnf,plain,
! [C,C1] :
( ( ? [P] :
( ~ incident_c(P,C)
& incident_c(P,C1) )
| part_of(C1,C) )
& ( ! [P] :
( incident_c(P,C)
| ~ incident_c(P,C1) )
| ~ part_of(C1,C) ) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [C1,C,P] :
( ( ( ~ incident_c(sk0(C,C1),C)
& incident_c(sk0(C,C1),C1) )
| part_of(C1,C) )
& ( incident_c(P,C)
| ~ incident_c(P,C1)
| ~ part_of(C1,C) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f0_nnf]) ).
cnf(c0,plain,
( incident_c(X2,X0)
| ~ incident_c(X2,X1)
| ~ part_of(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f16,conjecture,
! [C1,C2] :
( ( part_of(C2,C1)
& part_of(C1,C2) )
=> C1 = C2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',part_of_antisymmetry) ).
fof(f16_neg,negated_conjecture,
~ ! [C1,C2] :
( ( part_of(C2,C1)
& part_of(C1,C2) )
=> C1 = C2 ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
? [C1,C2] :
( C1 != C2
& part_of(C2,C1)
& part_of(C1,C2) ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
( sk13 != sk14
& part_of(sk14,sk13)
& part_of(sk13,sk14) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk13,sk14])],[f16_nnf]) ).
cnf(c48,plain,
part_of(sk13,sk14),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p51,plain,
( incident_c(X0,sk14)
| ~ incident_c(X0,sk13) ),
inference(resolution,[status(thm)],[c0,c48]) ).
cnf(p987,plain,
( incident_c(sk12(sk13,X0),sk14)
| sk13 = X0
| incident_c(sk12(sk13,X0),X0) ),
inference(resolution,[status(thm)],[c45,p51]) ).
cnf(p14445,plain,
( sk13 = sk14
| incident_c(sk12(sk13,sk14),sk14) ),
inference(factoring,[status(thm)],[p987]) ).
cnf(c46,plain,
( X0 = X1
| ~ incident_c(sk12(X0,X1),X0)
| ~ incident_c(sk12(X0,X1),X1) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p14491,plain,
( sk13 = sk14
| ~ incident_c(sk12(sk13,sk14),sk13)
| sk13 = sk14 ),
inference(resolution,[status(thm)],[p14445,c46]) ).
cnf(p14581,plain,
( ~ incident_c(sk12(sk13,sk14),sk13)
| sk13 = sk14 ),
inference(factoring,[status(thm)],[p14491]) ).
cnf(c49,plain,
part_of(sk14,sk13),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p52,plain,
( incident_c(X0,sk13)
| ~ incident_c(X0,sk14) ),
inference(resolution,[status(thm)],[c0,c49]) ).
cnf(p14480,plain,
( incident_c(sk12(sk13,sk14),sk13)
| sk13 = sk14 ),
inference(resolution,[status(thm)],[p14445,p52]) ).
cnf(p14582,plain,
( sk13 = sk14
| sk13 = sk14 ),
inference(resolution,[status(thm)],[p14581,p14480]) ).
cnf(p14583,plain,
sk13 = sk14,
inference(factoring,[status(thm)],[p14582]) ).
cnf(c50,plain,
sk13 != sk14,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p14584,plain,
$false,
inference(resolution,[status(thm)],[p14583,c50]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO082+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n016.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 10:50:25 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 49.86/7.00 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 49.86/7.00 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------