%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO524+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 : Sun Sep 27 07:18:02 AM UTC 2026
% Result : Theorem 1.77s 0.73s
% Output : CNFRefutation 1.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 2
% Syntax : Number of formulae : 14 ( 6 unt; 0 def)
% Number of atoms : 26 ( 25 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 21 ( 9 ~; 8 |; 4 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-3 aty)
% Number of variables : 18 ( 0 sgn 11 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(aSatz10_5,axiom,
! [Xa,Xb,Xp] :
( reflect(Xa,Xb,reflect(Xa,Xb,Xp)) = Xp
| Xa = Xb ),
file('theBenchmark.p',aSatz10_5) ).
fof(aSatz10_7,conjecture,
! [Xa,Xb,Xp,Xq] :
( Xp = Xq
| reflect(Xa,Xb,Xp) != reflect(Xa,Xb,Xq)
| Xa = Xb ),
file('theBenchmark.p',aSatz10_7) ).
fof(aSatz10_7_neg,negated_conjecture,
~ ! [Xa,Xb,Xp,Xq] :
( Xp = Xq
| reflect(Xa,Xb,Xp) != reflect(Xa,Xb,Xq)
| Xa = Xb ),
inference(assume_negation,[status(cth)],[aSatz10_7]) ).
cnf(c_483,plain,
( reflect(B,A,reflect(B,A,C)) = C
| A = B ),
inference(clausify,[status(thm)],[aSatz10_5]) ).
fof(nnf_200,plain,
? [Xa,Xb,Xp,Xq] :
( Xq != Xp
& reflect(Xa,Xb,Xq) = reflect(Xa,Xb,Xp)
& Xb != Xa ),
inference(fof_nnf,[status(thm)],[aSatz10_7_neg]) ).
fof(sk_aSatz10_7_neg,plain,
( sK2 != sK3
& reflect(sK1,sK0,sK2) = reflect(sK1,sK0,sK3)
& sK0 != sK1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(Xa,sK1),skolemize(Xb,sK0),skolemize(Xp,sK3),skolemize(Xq,sK2)],[nnf_200]) ).
cnf(c_493,negated_conjecture,
sK0 != sK1,
inference(split_conjunct,[status(thm)],[sk_aSatz10_7_neg]) ).
cnf(c_494,negated_conjecture,
reflect(sK1,sK0,sK2) = reflect(sK1,sK0,sK3),
inference(split_conjunct,[status(thm)],[sk_aSatz10_7_neg]) ).
cnf(c_495,negated_conjecture,
sK2 != sK3,
inference(split_conjunct,[status(thm)],[sk_aSatz10_7_neg]) ).
cnf(c_1425,plain,
( reflect(sK1,sK0,reflect(sK1,sK0,sK3)) = sK2
| sK0 = sK1 ),
inference(paramod,[status(thm)],[c_494,c_483]) ).
cnf(c_1420,negated_conjecture,
reflect(sK1,sK0,reflect(sK1,sK0,sK3)) = sK2,
inference(resolve,[status(thm)],[c_493,c_1425]) ).
cnf(c_1426,plain,
( sK2 = sK3
| sK0 = sK1 ),
inference(paramod,[status(thm)],[c_1420,c_483]) ).
cnf(c_1427,negated_conjecture,
sK2 = sK3,
inference(resolve,[status(thm)],[c_493,c_1426]) ).
cnf(c_1424,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_495,c_1427]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO524+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 13:42:12 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.02/0.36 % Process 1489419 was started by sandbox2 on n015,
% 0.02/0.36 % Fri Sep 25 13:42:12 2026
% 0.02/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.02/0.41
% 0.02/0.41 % From the command line: assign(max_seconds, 300).
% 0.02/0.41
% 0.02/0.41 % SInE: 155 to sos, 48 to usable, of 203 axioms (tolerance 2.00, depth 0 fixpoint).
% 1.77/0.73
% 1.77/0.73 % SZS status Theorem for theBenchmark
% 1.77/0.73
% 1.77/0.73 % Proof 1 at 0.15 (+ 0.04) seconds.
% 1.77/0.73 % Length of proof is 8.
% 1.77/0.73 % Level of proof is 3.
% 1.77/0.73 % Maximum clause weight is 12.000.
% 1.77/0.73 % Given clauses 64.
% 1.77/0.73
% 1.77/0.73 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------