%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP642+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:30:37 AM UTC 2026
% Result : Theorem 89.81s 13.57s
% Output : CNFRefutation 89.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 6
% Syntax : Number of formulae : 39 ( 21 unt; 0 def)
% Number of atoms : 101 ( 16 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 101 ( 39 ~; 30 |; 25 &)
% ( 1 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 21 ( 2 sgn 9 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(rc1_xboole_0,axiom,
? [A] : v1_xboole_0(A),
file('theBenchmark.p',rc1_xboole_0) ).
fof(d5_xboole_0,axiom,
! [A] :
( v1_xboole_0(A)
<=> A = k1_xboole_0 ),
file('theBenchmark.p',d5_xboole_0) ).
fof(t19_latsubgr,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_group_2(B,A)
& v1_group_1(B) )
=> r2_hidden(k2_group_1(A),k1_funct_1(k1_latsubgr(A),B)) ) ),
file('theBenchmark.p',t19_latsubgr) ).
fof(t7_boole,axiom,
! [A,B] :
~ ( v1_xboole_0(B)
& r2_hidden(A,B) ),
file('theBenchmark.p',t7_boole) ).
fof(t20_latsubgr,conjecture,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_group_2(B,A)
& v1_group_1(B) )
=> k1_funct_1(k1_latsubgr(A),B) != k1_xboole_0 ) ),
file('theBenchmark.p',t20_latsubgr) ).
fof(t20_latsubgr_neg,negated_conjecture,
~ ! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_group_2(B,A)
& v1_group_1(B) )
=> k1_funct_1(k1_latsubgr(A),B) != k1_xboole_0 ) ),
inference(assume_negation,[status(cth)],[t20_latsubgr]) ).
cnf(c_939,plain,
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(clausify,[status(thm)],[t7_boole]) ).
fof(t51_card_1,axiom,
np__0 = k1_xboole_0,
file('theBenchmark.p',t51_card_1) ).
cnf(c_1422,plain,
np__0 = k1_xboole_0,
inference(clausify,[status(thm)],[t51_card_1]) ).
cnf(c_1423,plain,
k1_xboole_0 = np__0,
inference(copy,[status(thm)],[c_1422]) ).
fof(nnf_8,plain,
? [A] : v1_xboole_0(A),
inference(fof_nnf,[status(thm)],[rc1_xboole_0]) ).
fof(sk_rc1_xboole_0,plain,
v1_xboole_0(sK0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(A,sK0)],[nnf_8]) ).
cnf(c_2224,plain,
v1_xboole_0(sK0),
inference(split_conjunct,[status(thm)],[sk_rc1_xboole_0]) ).
cnf(c_2248,plain,
( k1_xboole_0 = A
| ~ v1_xboole_0(A) ),
inference(clausify,[status(thm)],[d5_xboole_0]) ).
cnf(c_2854,plain,
( r2_hidden(k2_group_1(A),k1_funct_1(k1_latsubgr(A),B))
| ~ m1_group_2(B,A)
| ~ v1_group_1(B)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t19_latsubgr]) ).
fof(nnf_925,plain,
? [A] :
( ? [B] :
( k1_funct_1(k1_latsubgr(A),B) = k1_xboole_0
& m1_group_2(B,A)
& v1_group_1(B) )
& l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t20_latsubgr_neg]) ).
fof(sk_t20_latsubgr_neg,plain,
( k1_funct_1(k1_latsubgr(sK1),sK2) = k1_xboole_0
& m1_group_2(sK2,sK1)
& v1_group_1(sK2)
& l1_group_1(sK1)
& v4_group_1(sK1)
& v3_group_1(sK1)
& ~ v3_struct_0(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(A,sK1),skolemize(B,sK2)],[nnf_925]) ).
cnf(c_2855,negated_conjecture,
~ v3_struct_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t20_latsubgr_neg]) ).
cnf(c_2856,negated_conjecture,
v3_group_1(sK1),
inference(split_conjunct,[status(thm)],[sk_t20_latsubgr_neg]) ).
cnf(c_2857,negated_conjecture,
v4_group_1(sK1),
inference(split_conjunct,[status(thm)],[sk_t20_latsubgr_neg]) ).
cnf(c_2858,negated_conjecture,
l1_group_1(sK1),
inference(split_conjunct,[status(thm)],[sk_t20_latsubgr_neg]) ).
cnf(c_2859,negated_conjecture,
v1_group_1(sK2),
inference(split_conjunct,[status(thm)],[sk_t20_latsubgr_neg]) ).
cnf(c_2860,negated_conjecture,
m1_group_2(sK2,sK1),
inference(split_conjunct,[status(thm)],[sk_t20_latsubgr_neg]) ).
cnf(c_2861,negated_conjecture,
k1_funct_1(k1_latsubgr(sK1),sK2) = k1_xboole_0,
inference(split_conjunct,[status(thm)],[sk_t20_latsubgr_neg]) ).
cnf(c_2862,negated_conjecture,
k1_xboole_0 = k1_funct_1(k1_latsubgr(sK1),sK2),
inference(copy,[status(thm)],[c_2861]) ).
cnf(c_3145,plain,
( k1_funct_1(k1_latsubgr(sK1),sK2) = A
| ~ v1_xboole_0(A) ),
inference(paramod,[status(thm)],[c_2862,c_2248]) ).
cnf(c_3202,plain,
k1_funct_1(k1_latsubgr(sK1),sK2) = np__0,
inference(paramod,[status(thm)],[c_2862,c_1423]) ).
cnf(c_3421,plain,
( np__0 = A
| ~ v1_xboole_0(A) ),
inference(paramod,[status(thm)],[c_3202,c_3145]) ).
cnf(c_8682,plain,
~ r2_hidden(A,sK0),
inference(resolve,[status(thm)],[c_2224,c_939]) ).
cnf(c_8845,plain,
np__0 = sK0,
inference(resolve,[status(thm)],[c_3421,c_2224]) ).
cnf(c_9386,plain,
k1_funct_1(k1_latsubgr(sK1),sK2) = sK0,
inference(paramod,[status(thm)],[c_8845,c_3202]) ).
cnf(c_25618,negated_conjecture,
( r2_hidden(k2_group_1(sK1),k1_funct_1(k1_latsubgr(sK1),sK2))
| ~ v1_group_1(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_2854,c_2860]) ).
cnf(c_25619,negated_conjecture,
( r2_hidden(k2_group_1(sK1),sK0)
| ~ v1_group_1(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_9386,c_25618]) ).
cnf(c_25620,negated_conjecture,
( r2_hidden(k2_group_1(sK1),sK0)
| ~ v1_group_1(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(resolve,[status(thm)],[c_2855,c_25619]) ).
cnf(c_25621,negated_conjecture,
( r2_hidden(k2_group_1(sK1),sK0)
| ~ v1_group_1(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1) ),
inference(resolve,[status(thm)],[c_2856,c_25620]) ).
cnf(c_25622,negated_conjecture,
( r2_hidden(k2_group_1(sK1),sK0)
| ~ v1_group_1(sK2)
| ~ l1_group_1(sK1) ),
inference(resolve,[status(thm)],[c_2857,c_25621]) ).
cnf(c_25623,negated_conjecture,
( r2_hidden(k2_group_1(sK1),sK0)
| ~ v1_group_1(sK2) ),
inference(resolve,[status(thm)],[c_2858,c_25622]) ).
cnf(c_25624,negated_conjecture,
r2_hidden(k2_group_1(sK1),sK0),
inference(resolve,[status(thm)],[c_2859,c_25623]) ).
cnf(c_25617,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_8682,c_25624]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP642+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n018.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Fri Sep 25 15:22:08 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.38 % Process 2293436 was started by sandbox2 on n018,
% 0.11/0.38 % Fri Sep 25 15:22:08 2026
% 0.11/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 89.81/13.57
% 89.81/13.57 % SInE (scan): 633 to sos (tol 1.5x), 299 to usable (tol 2.0x), 4726 zapped, of 5658 axioms (depth 3).
% 89.81/13.57
% 89.81/13.57 % From the command line: assign(max_seconds, 300).
% 89.81/13.57
% 89.81/13.57 % given #500 (F,wt=15): 16023 -r1_tarski(k2_tarski(A,B),B). [resolve(8661,a,1272,a)].
% 89.81/13.57
% 89.81/13.57 % given #1000 (W,wt=16): 9340 v1_relat_1(f113(A)) | c1 = A. [back_rewrite(3249),rewrite([8845(3)])].
% 89.81/13.57
% 89.81/13.57 % given #1500 (F,wt=18): 21275 -r2_hidden(k2_tarski(A,B),C) | -r2_hidden(C,B). [resolve(2678,a,8661,a)].
% 89.81/13.57
% 89.81/13.57 % SZS status Theorem for theBenchmark
% 89.81/13.57
% 89.81/13.57 % Proof 1 at 11.31 (+ 1.16) seconds.
% 89.81/13.57 % Length of proof is 26.
% 89.81/13.57 % Level of proof is 7.
% 89.81/13.57 % Maximum clause weight is 107.000.
% 89.81/13.57 % Given clauses 1588.
% 89.81/13.57
% 89.81/13.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------