%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO146-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:17:11 AM UTC 2026
% Result : Unsatisfiable 80.13s 22.45s
% Output : CNFRefutation 80.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 5
% Syntax : Number of formulae : 19 ( 6 unt; 0 def)
% Number of atoms : 32 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 24 ( 11 ~; 13 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 16 ( 0 sgn 8 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(connect_defn_1,axiom,
! [VAR_0,VAR_1,VAR_2] :
( once(at_the_same_time(at(VAR_0,VAR_2),at(VAR_1,VAR_2)))
| ~ connect(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',connect_defn_1) ).
cnf(c_131,plain,
( once(at_the_same_time(at(A,C),at(B,C)))
| ~ connect(A,B,C) ),
inference(clausify,[status(thm)],[connect_defn_1]) ).
fof(connect_defn_2,axiom,
! [VAR_0,VAR_1,VAR_2] :
( connect(VAR_0,VAR_2,VAR_1)
| ~ once(at_the_same_time(at(VAR_0,VAR_1),at(VAR_2,VAR_1))) ),
file('theBenchmark.p',connect_defn_2) ).
cnf(c_132,plain,
( connect(A,C,B)
| ~ once(at_the_same_time(at(A,B),at(C,B))) ),
inference(clausify,[status(thm)],[connect_defn_2]) ).
fof(symmetry_of_at_the_same_time_3,axiom,
! [VAR_0,VAR_1] :
( once(at_the_same_time(VAR_1,VAR_0))
| ~ once(at_the_same_time(VAR_0,VAR_1)) ),
file('theBenchmark.p',symmetry_of_at_the_same_time_3) ).
cnf(c_133,plain,
( once(at_the_same_time(B,A))
| ~ once(at_the_same_time(A,B)) ),
inference(clausify,[status(thm)],[symmetry_of_at_the_same_time_3]) ).
fof(t12_156,axiom,
( connect(sk28,sk27,sk29)
| connect(sk27,sk28,sk29) ),
file('theBenchmark.p',t12_156) ).
cnf(c_145,plain,
( connect(sk28,sk27,sk29)
| connect(sk27,sk28,sk29) ),
inference(clausify,[status(thm)],[t12_156]) ).
fof(t12_159,axiom,
( ~ connect(sk27,sk28,sk29)
| ~ connect(sk28,sk27,sk29) ),
file('theBenchmark.p',t12_159) ).
cnf(c_146,plain,
( ~ connect(sk27,sk28,sk29)
| ~ connect(sk28,sk27,sk29) ),
inference(clausify,[status(thm)],[t12_159]) ).
cnf(c_438,plain,
( once(at_the_same_time(at(sk28,sk29),at(sk27,sk29)))
| connect(sk27,sk28,sk29) ),
inference(resolve,[status(thm)],[c_145,c_131]) ).
cnf(c_2683,plain,
( once(at_the_same_time(at(sk27,sk29),at(sk28,sk29)))
| once(at_the_same_time(at(sk28,sk29),at(sk27,sk29))) ),
inference(resolve,[status(thm)],[c_438,c_131]) ).
cnf(c_30546,plain,
( once(at_the_same_time(at(sk27,sk29),at(sk28,sk29)))
| once(at_the_same_time(at(sk27,sk29),at(sk28,sk29))) ),
inference(resolve,[status(thm)],[c_2683,c_133]) ).
cnf(c_30266,plain,
once(at_the_same_time(at(sk27,sk29),at(sk28,sk29))),
inference(copy,[status(thm)],[c_30546]) ).
cnf(c_30271,plain,
once(at_the_same_time(at(sk28,sk29),at(sk27,sk29))),
inference(resolve,[status(thm)],[c_30266,c_133]) ).
cnf(c_30272,plain,
connect(sk27,sk28,sk29),
inference(resolve,[status(thm)],[c_30266,c_132]) ).
cnf(c_30273,plain,
~ connect(sk28,sk27,sk29),
inference(resolve,[status(thm)],[c_30272,c_146]) ).
cnf(c_30547,plain,
connect(sk28,sk27,sk29),
inference(resolve,[status(thm)],[c_30271,c_132]) ).
cnf(c_30545,plain,
$false,
inference(resolve,[status(thm)],[c_30273,c_30547]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO146-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.36 % Computer : n007.cluster.edu
% 0.07/0.36 % Model : x86_64 x86_64
% 0.07/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.36 % Memory : 8046.5625MB
% 0.07/0.36 % OS : Linux 6.8.0-71-generic
% 0.07/0.36 % CPULimit : 300
% 0.07/0.36 % WCLimit : 300
% 0.07/0.36 % DateTime : Fri Sep 25 12:53:53 UTC 2026
% 0.07/0.37 % CPUTime :
% 0.07/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.37 % Process 1045781 was started by sandbox on n007,
% 0.07/0.37 % Fri Sep 25 12:53:53 2026
% 0.07/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.07/0.38
% 0.07/0.38 % From the command line: assign(max_seconds, 300).
% 80.13/22.45
% 80.13/22.45 % given #500 (A,wt=39): 338 -incident_c(ax0_sk2(A,B,C),D) | incident_c(ax0_sk5(D,C,ax0_sk2(A,B,C)),D) | meet(ax0_sk2(A,B,C),C,D) | incident_c(ax0_sk2(A,B,C),B) | incident_c(ax0_sk2(A,B,C),A) | sum(B,A) = C. [resolve(101,a,80,a)].
% 80.13/22.45
% 80.13/22.45 % given #1000 (T,wt=11): 13156 incident_c(ax2_sk6(A),sum(sum(B,sum(ax2_sk3(A),C)),D)). [resolve(4199,a,1886,a(flip)),rewrite([1886(10)])].
% 80.13/22.45
% 80.13/22.45 % given #1500 (T,wt=15): 7857 incident_c(ax0_sk8(A),B) | incident_c(ax0_sk1(A,ax2_sk3(C)),A) | incident_o(ax0_sk1(A,B),C). [resolve(1303,c,118,a)].
% 80.13/22.45
% 80.13/22.45 % given #2000 (A,wt=21): 894 incident_o(ax2_sk1(A,ax0_sk6(ax2_sk3(A))),A) | ax0_sk6(ax2_sk3(A)) = B | -incident_o(B,A) | ordered_by(A,ax0_sk6(ax2_sk3(A)),B). [resolve(883,a,177,a)].
% 80.13/22.45
% 80.13/22.45 % SZS status Unsatisfiable for theBenchmark
% 80.13/22.45
% 80.13/22.45 % Proof 1 at 8.32 (+ 2.03) seconds.
% 80.13/22.45 % Length of proof is 12.
% 80.13/22.45 % Level of proof is 6.
% 80.13/22.45 % Maximum clause weight is 16.000.
% 80.13/22.45 % Given clauses 2118.
% 80.13/22.45
% 80.13/22.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------