%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYO607+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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 : Thu Sep 24 09:12:10 AM UTC 2026
% Result : Theorem 2.50s 18.62s
% Output : Proof 2.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 5
% Syntax : Number of formulae : 131 ( 66 unt; 0 def)
% Number of atoms : 392 ( 0 equ)
% Maximal formula atoms : 19 ( 2 avg)
% Number of connectives : 426 ( 165 ~; 181 |; 77 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 2 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-1 aty)
% Number of variables : 203 ( 10 sgn 127 !; 51 ?)
% Comments :
%------------------------------------------------------------------------------
fof(nc6,conjecture,
( ( ~ ? [A] :
! [B] : g_true_only(A,B)
& ? [A] :
( ~ ? [B] : g_false_only(A,B)
& ? [B] : g_both(A,B) )
& ~ ? [A] :
( ? [B] : g_false_only(A,B)
& g_false_only(a,A) )
& ? [A] :
( ~ ! [B] : g_true_only(A,B)
& ~ g_true_only(a,A)
& ( ( ~ ? [B] : g_false_only(A,B)
& ? [B] : g_both(A,B) )
| g_both(a,A) ) ) )
| ? [A] :
! [B] : g_true_only(A,B)
| ? [A] :
( ? [B] : g_false_only(A,B)
& g_false_only(a,A) ) ),
file('theBenchmark.p',nc6) ).
fof(true_only_g,axiom,
! [X_2,X_1] :
( g_true_only(X_2,X_1)
<=> ( ~ g_false(X_2,X_1)
& g_true(X_2,X_1) ) ),
file('theBenchmark.p',true_only_g) ).
fof(both_g,axiom,
! [X_2,X_1] :
( g_both(X_2,X_1)
<=> ( g_false(X_2,X_1)
& g_true(X_2,X_1) ) ),
file('theBenchmark.p',both_g) ).
fof(false_only_g,axiom,
! [X_2,X_1] :
( g_false_only(X_2,X_1)
<=> ( ~ g_true(X_2,X_1)
& g_false(X_2,X_1) ) ),
file('theBenchmark.p',false_only_g) ).
fof(exhaustion_g,axiom,
! [X_2,X_1] :
( g_false_only(X_2,X_1)
| g_both(X_2,X_1)
| g_true_only(X_2,X_1) ),
file('theBenchmark.p',exhaustion_g) ).
fof(f_1_1,negated_conjecture,
~ ( ( ~ ? [A] :
! [B] : g_true_only(A,B)
& ? [A] :
( ~ ? [B] : g_false_only(A,B)
& ? [B] : g_both(A,B) )
& ~ ? [A] :
( ? [B] : g_false_only(A,B)
& g_false_only(a,A) )
& ? [A] :
( ~ ! [B] : g_true_only(A,B)
& ~ g_true_only(a,A)
& ( ( ~ ? [B] : g_false_only(A,B)
& ? [B] : g_both(A,B) )
| g_both(a,A) ) ) )
| ? [A] :
! [B] : g_true_only(A,B)
| ? [A] :
( ? [B] : g_false_only(A,B)
& g_false_only(a,A) ) ),
inference(negate,[status(cth)],[nc6]) ).
fof(f_1_2,negated_conjecture,
( ( ? [A] :
! [B] : g_true_only(A,B)
| ! [A] :
( ? [B] : g_false_only(A,B)
| ! [B] : ~ g_both(A,B) )
| ? [A] :
( ? [B] : g_false_only(A,B)
& g_false_only(a,A) )
| ! [A] :
( ! [B] : g_true_only(A,B)
| g_true_only(a,A)
| ( ( ? [B] : g_false_only(A,B)
| ! [B] : ~ g_both(A,B) )
& ~ g_both(a,A) ) ) )
& ! [A] :
? [B] : ~ g_true_only(A,B)
& ! [A] :
( ! [B] : ~ g_false_only(A,B)
| ~ g_false_only(a,A) ) ),
inference(fof_nnf,[status(thm)],[f_1_1]) ).
fof(f_1_3,negated_conjecture,
( ( ? [U_14] :
! [U_13] : g_true_only(U_14,U_13)
| ! [U_12] :
( ? [U_11] : g_false_only(U_12,U_11)
| ! [U_10] : ~ g_both(U_12,U_10) )
| ? [U_9] :
( ? [U_8] : g_false_only(U_9,U_8)
& g_false_only(a,U_9) )
| ! [U_7] :
( ! [U_6] : g_true_only(U_7,U_6)
| g_true_only(a,U_7)
| ( ( ? [U_5] : g_false_only(U_7,U_5)
| ! [U_4] : ~ g_both(U_7,U_4) )
& ~ g_both(a,U_7) ) ) )
& ! [U_3] :
? [U_2] : ~ g_true_only(U_3,U_2)
& ! [U_1] :
( ! [U_0] : ~ g_false_only(U_1,U_0)
| ~ g_false_only(a,U_1) ) ),
inference(variable_rename,[status(thm)],[f_1_2]) ).
fof(f_1_4,negated_conjecture,
( ( ? [U_14] :
! [U_13] : g_true_only(U_14,U_13)
| ! [U_12] :
( ? [U_11] : g_false_only(U_12,U_11)
| ! [U_10] : ~ g_both(U_12,U_10) )
| ? [U_9] :
( ? [U_8] : g_false_only(U_9,U_8)
& g_false_only(a,U_9) )
| ! [U_7] :
( ! [U_6] : g_true_only(U_7,U_6)
| g_true_only(a,U_7)
| ( ( ? [U_5] : g_false_only(U_7,U_5)
| ! [U_4] : ~ g_both(U_7,U_4) )
& ~ g_both(a,U_7) ) ) )
& ! [U_3] : ~ g_true_only(U_3,sK1(U_3))
& ! [U_1] :
( ! [U_0] : ~ g_false_only(U_1,U_0)
| ~ g_false_only(a,U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_2,sK1(U_3))],[f_1_3]) ).
fof(f_1_5,negated_conjecture,
( ( ? [U_14] :
! [U_13] : g_true_only(U_14,U_13)
| ! [U_12] :
( ? [U_11] : g_false_only(U_12,U_11)
| ! [U_10] : ~ g_both(U_12,U_10) )
| ? [U_9] :
( ? [U_8] : g_false_only(U_9,U_8)
& g_false_only(a,U_9) )
| ! [U_7] :
( ! [U_6] : g_true_only(U_7,U_6)
| g_true_only(a,U_7)
| ( ( g_false_only(U_7,sK2(U_7))
| ! [U_4] : ~ g_both(U_7,U_4) )
& ~ g_both(a,U_7) ) ) )
& ! [U_3] : ~ g_true_only(U_3,sK1(U_3))
& ! [U_1] :
( ! [U_0] : ~ g_false_only(U_1,U_0)
| ~ g_false_only(a,U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_5,sK2(U_7))],[f_1_4]) ).
fof(f_1_6,negated_conjecture,
( ( ? [U_14] :
! [U_13] : g_true_only(U_14,U_13)
| ! [U_12] :
( ? [U_11] : g_false_only(U_12,U_11)
| ! [U_10] : ~ g_both(U_12,U_10) )
| ( ? [U_8] : g_false_only(sK3,U_8)
& g_false_only(a,sK3) )
| ! [U_7] :
( ! [U_6] : g_true_only(U_7,U_6)
| g_true_only(a,U_7)
| ( ( g_false_only(U_7,sK2(U_7))
| ! [U_4] : ~ g_both(U_7,U_4) )
& ~ g_both(a,U_7) ) ) )
& ! [U_3] : ~ g_true_only(U_3,sK1(U_3))
& ! [U_1] :
( ! [U_0] : ~ g_false_only(U_1,U_0)
| ~ g_false_only(a,U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_9,sK3)],[f_1_5]) ).
fof(f_1_7,negated_conjecture,
( ( ? [U_14] :
! [U_13] : g_true_only(U_14,U_13)
| ! [U_12] :
( ? [U_11] : g_false_only(U_12,U_11)
| ! [U_10] : ~ g_both(U_12,U_10) )
| ( g_false_only(sK3,sK4)
& g_false_only(a,sK3) )
| ! [U_7] :
( ! [U_6] : g_true_only(U_7,U_6)
| g_true_only(a,U_7)
| ( ( g_false_only(U_7,sK2(U_7))
| ! [U_4] : ~ g_both(U_7,U_4) )
& ~ g_both(a,U_7) ) ) )
& ! [U_3] : ~ g_true_only(U_3,sK1(U_3))
& ! [U_1] :
( ! [U_0] : ~ g_false_only(U_1,U_0)
| ~ g_false_only(a,U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_8,sK4)],[f_1_6]) ).
fof(f_1_8,negated_conjecture,
( ( ? [U_14] :
! [U_13] : g_true_only(U_14,U_13)
| ! [U_12] :
( g_false_only(U_12,sK5(U_12))
| ! [U_10] : ~ g_both(U_12,U_10) )
| ( g_false_only(sK3,sK4)
& g_false_only(a,sK3) )
| ! [U_7] :
( ! [U_6] : g_true_only(U_7,U_6)
| g_true_only(a,U_7)
| ( ( g_false_only(U_7,sK2(U_7))
| ! [U_4] : ~ g_both(U_7,U_4) )
& ~ g_both(a,U_7) ) ) )
& ! [U_3] : ~ g_true_only(U_3,sK1(U_3))
& ! [U_1] :
( ! [U_0] : ~ g_false_only(U_1,U_0)
| ~ g_false_only(a,U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_11,sK5(U_12))],[f_1_7]) ).
fof(f_1_9,negated_conjecture,
( ( ! [U_13] : g_true_only(sK6,U_13)
| ! [U_12] :
( g_false_only(U_12,sK5(U_12))
| ! [U_10] : ~ g_both(U_12,U_10) )
| ( g_false_only(sK3,sK4)
& g_false_only(a,sK3) )
| ! [U_7] :
( ! [U_6] : g_true_only(U_7,U_6)
| g_true_only(a,U_7)
| ( ( g_false_only(U_7,sK2(U_7))
| ! [U_4] : ~ g_both(U_7,U_4) )
& ~ g_both(a,U_7) ) ) )
& ! [U_3] : ~ g_true_only(U_3,sK1(U_3))
& ! [U_1] :
( ! [U_0] : ~ g_false_only(U_1,U_0)
| ~ g_false_only(a,U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_14,sK6)],[f_1_8]) ).
fof(f_1_10,negated_conjecture,
( ( g_false_only(sK3,sK4)
| ~ sP1 )
& ( g_false_only(a,sK3)
| ~ sP1 )
& ! [U_7,U_4] :
( g_false_only(U_7,sK2(U_7))
| ~ g_both(U_7,U_4)
| ~ sP0(U_7,U_4) )
& ! [U_7,U_4] :
( ~ g_both(a,U_7)
| ~ sP0(U_7,U_4) )
& ! [U_7,U_13,U_10,U_12,U_6,U_4] :
( g_true_only(sK6,U_13)
| g_false_only(U_12,sK5(U_12))
| ~ g_both(U_12,U_10)
| sP1
| g_true_only(U_7,U_6)
| g_true_only(a,U_7)
| sP0(U_7,U_4) )
& ! [U_3] : ~ g_true_only(U_3,sK1(U_3))
& ! [U_1,U_0] :
( ~ g_false_only(U_1,U_0)
| ~ g_false_only(a,U_1) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1])],[f_1_9]) ).
cnf(f_1_11,negated_conjecture,
( ~ g_false_only(U_1,U_0)
| ~ g_false_only(a,U_1) ),
inference(clausify,[status(thm)],[f_1_10]) ).
cnf(f_1_12,negated_conjecture,
~ g_true_only(U_3,sK1(U_3)),
inference(clausify,[status(thm)],[f_1_10]) ).
cnf(f_1_13,negated_conjecture,
( g_true_only(sK6,U_13)
| g_false_only(U_12,sK5(U_12))
| ~ g_both(U_12,U_10)
| sP1
| g_true_only(U_7,U_6)
| g_true_only(a,U_7)
| sP0(U_7,U_4) ),
inference(clausify,[status(thm)],[f_1_10]) ).
cnf(f_1_14,negated_conjecture,
( ~ g_both(a,U_7)
| ~ sP0(U_7,U_4) ),
inference(clausify,[status(thm)],[f_1_10]) ).
cnf(f_1_15,negated_conjecture,
( g_false_only(U_7,sK2(U_7))
| ~ g_both(U_7,U_4)
| ~ sP0(U_7,U_4) ),
inference(clausify,[status(thm)],[f_1_10]) ).
cnf(f_1_16,negated_conjecture,
( g_false_only(a,sK3)
| ~ sP1 ),
inference(clausify,[status(thm)],[f_1_10]) ).
cnf(f_1_17,negated_conjecture,
( g_false_only(sK3,sK4)
| ~ sP1 ),
inference(clausify,[status(thm)],[f_1_10]) ).
fof(f_2_1,plain,
! [X_2,X_1] :
( ( g_true_only(X_2,X_1)
| g_false(X_2,X_1)
| ~ g_true(X_2,X_1) )
& ( ( ~ g_false(X_2,X_1)
& g_true(X_2,X_1) )
| ~ g_true_only(X_2,X_1) ) ),
inference(fof_nnf,[status(thm)],[true_only_g]) ).
fof(f_2_2,plain,
! [U_16,U_15] :
( ( g_true_only(U_16,U_15)
| g_false(U_16,U_15)
| ~ g_true(U_16,U_15) )
& ( ( ~ g_false(U_16,U_15)
& g_true(U_16,U_15) )
| ~ g_true_only(U_16,U_15) ) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
( ! [U_20,U_18] :
( g_true_only(U_20,U_18)
| g_false(U_20,U_18)
| ~ g_true(U_20,U_18) )
& ! [U_19,U_17] :
( ( ~ g_false(U_19,U_17)
& g_true(U_19,U_17) )
| ~ g_true_only(U_19,U_17) ) ),
inference(miniscope,[status(thm)],[f_2_2]) ).
cnf(f_2_5,plain,
( ~ g_false(U_19,U_17)
| ~ g_true_only(U_19,U_17) ),
inference(clausify,[status(thm)],[f_2_3]) ).
fof(f_3_1,plain,
! [X_2,X_1] :
( ( g_both(X_2,X_1)
| ~ g_false(X_2,X_1)
| ~ g_true(X_2,X_1) )
& ( ( g_false(X_2,X_1)
& g_true(X_2,X_1) )
| ~ g_both(X_2,X_1) ) ),
inference(fof_nnf,[status(thm)],[both_g]) ).
fof(f_3_2,plain,
! [U_22,U_21] :
( ( g_both(U_22,U_21)
| ~ g_false(U_22,U_21)
| ~ g_true(U_22,U_21) )
& ( ( g_false(U_22,U_21)
& g_true(U_22,U_21) )
| ~ g_both(U_22,U_21) ) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
( ! [U_26,U_24] :
( g_both(U_26,U_24)
| ~ g_false(U_26,U_24)
| ~ g_true(U_26,U_24) )
& ! [U_25,U_23] :
( ( g_false(U_25,U_23)
& g_true(U_25,U_23) )
| ~ g_both(U_25,U_23) ) ),
inference(miniscope,[status(thm)],[f_3_2]) ).
cnf(f_3_5,plain,
( g_false(U_25,U_23)
| ~ g_both(U_25,U_23) ),
inference(clausify,[status(thm)],[f_3_3]) ).
fof(f_4_1,plain,
! [X_2,X_1] :
( ( g_false_only(X_2,X_1)
| g_true(X_2,X_1)
| ~ g_false(X_2,X_1) )
& ( ( ~ g_true(X_2,X_1)
& g_false(X_2,X_1) )
| ~ g_false_only(X_2,X_1) ) ),
inference(fof_nnf,[status(thm)],[false_only_g]) ).
fof(f_4_2,plain,
! [U_28,U_27] :
( ( g_false_only(U_28,U_27)
| g_true(U_28,U_27)
| ~ g_false(U_28,U_27) )
& ( ( ~ g_true(U_28,U_27)
& g_false(U_28,U_27) )
| ~ g_false_only(U_28,U_27) ) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
( ! [U_32,U_30] :
( g_false_only(U_32,U_30)
| g_true(U_32,U_30)
| ~ g_false(U_32,U_30) )
& ! [U_31,U_29] :
( ( ~ g_true(U_31,U_29)
& g_false(U_31,U_29) )
| ~ g_false_only(U_31,U_29) ) ),
inference(miniscope,[status(thm)],[f_4_2]) ).
cnf(f_4_4,plain,
( g_false(U_31,U_29)
| ~ g_false_only(U_31,U_29) ),
inference(clausify,[status(thm)],[f_4_3]) ).
fof(f_5_1,plain,
! [X_2,X_1] :
( g_false_only(X_2,X_1)
| g_both(X_2,X_1)
| g_true_only(X_2,X_1) ),
inference(fof_nnf,[status(thm)],[exhaustion_g]) ).
fof(f_5_2,plain,
! [U_34,U_33] :
( g_false_only(U_34,U_33)
| g_both(U_34,U_33)
| g_true_only(U_34,U_33) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
cnf(f_5_3,plain,
( g_false_only(U_34,U_33)
| g_both(U_34,U_33)
| g_true_only(U_34,U_33) ),
inference(clausify,[status(thm)],[f_5_2]) ).
cnf(t1,plain,
( ~ g_false_only(sK1(a),sK1(sK1(a)))
| ~ g_false_only(a,sK1(a)) ),
inference(start,[status(thm),parent(0:0)],[f_1_11]) ).
cnf(t2,plain,
( g_both(a,sK1(a))
| g_true_only(a,sK1(a))
| g_false_only(a,sK1(a)) ),
inference(extension,[status(thm),parent(t1:1)],[f_5_3]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
~ g_true_only(a,sK1(a)),
inference(extension,[status(thm),parent(t2:2)],[f_1_12]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(l2,lemma,
~ g_true_only(a,sK1(a)),
inference(lemma,[status(cth),parent(t2:2),below(t1:1)],[t2:2]) ).
cnf(t6,plain,
( g_true_only(a,sK1(a))
| g_true_only(sK1(a),sK1(sK1(a)))
| sP1
| g_true_only(sK6,sK1(sK6))
| g_false_only(a,sK5(a))
| sP0(sK1(a),U_232)
| ~ g_both(a,sK1(a)) ),
inference(extension,[status(thm),parent(t2:3)],[f_1_13]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t2:3]) ).
cnf(t8,plain,
( ~ g_both(a,sK1(a))
| ~ sP0(sK1(a),U_232) ),
inference(extension,[status(thm),parent(t6:2)],[f_1_14]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
$false,
inference(reduction,[status(thm),parent(t8:2)],[t8:2,t2:3]) ).
cnf(t11,plain,
( ~ g_false_only(sK5(a),sK5(sK5(a)))
| ~ g_false_only(a,sK5(a)) ),
inference(extension,[status(thm),parent(t6:3)],[f_1_11]) ).
cnf(t12,plain,
$false,
inference(connection,[status(thm),parent(t11:1)],[t11:1,t6:3]) ).
cnf(t13,plain,
( g_true_only(a,sK1(a))
| g_true_only(sK1(a),sK1(sK1(a)))
| sP1
| ~ g_both(sK5(a),sK1(sK5(a)))
| g_true_only(sK6,sK1(sK6))
| sP0(sK1(a),U_242)
| g_false_only(sK5(a),sK5(sK5(a))) ),
inference(extension,[status(thm),parent(t11:2)],[f_1_13]) ).
cnf(t14,plain,
$false,
inference(connection,[status(thm),parent(t13:1)],[t13:1,t11:2]) ).
cnf(t15,plain,
( ~ g_both(a,sK1(a))
| ~ sP0(sK1(a),U_242) ),
inference(extension,[status(thm),parent(t13:2)],[f_1_14]) ).
cnf(t16,plain,
$false,
inference(connection,[status(thm),parent(t15:1)],[t15:1,t13:2]) ).
cnf(t17,plain,
$false,
inference(reduction,[status(thm),parent(t15:2)],[t15:2,t2:3]) ).
cnf(t18,plain,
~ g_true_only(sK6,sK1(sK6)),
inference(extension,[status(thm),parent(t13:3)],[f_1_12]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t13:3]) ).
cnf(t20,plain,
( g_false_only(sK5(a),sK1(sK5(a)))
| g_true_only(sK5(a),sK1(sK5(a)))
| g_both(sK5(a),sK1(sK5(a))) ),
inference(extension,[status(thm),parent(t13:4)],[f_5_3]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t13:4]) ).
cnf(t22,plain,
~ g_true_only(sK5(a),sK1(sK5(a))),
inference(extension,[status(thm),parent(t20:2)],[f_1_12]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t20:2]) ).
cnf(t24,plain,
( ~ g_false_only(a,sK5(a))
| ~ g_false_only(sK5(a),sK1(sK5(a))) ),
inference(extension,[status(thm),parent(t20:3)],[f_1_11]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t20:3]) ).
cnf(t26,plain,
$false,
inference(reduction,[status(thm),parent(t24:2)],[t24:2,t6:3]) ).
cnf(t27,plain,
( g_false_only(sK3,sK4)
| ~ sP1 ),
inference(extension,[status(thm),parent(t13:5)],[f_1_17]) ).
cnf(t28,plain,
$false,
inference(connection,[status(thm),parent(t27:1)],[t27:1,t13:5]) ).
cnf(t29,plain,
( ~ g_false_only(a,sK3)
| ~ g_false_only(sK3,sK4) ),
inference(extension,[status(thm),parent(t27:2)],[f_1_11]) ).
cnf(t30,plain,
$false,
inference(connection,[status(thm),parent(t29:1)],[t29:1,t27:2]) ).
cnf(t31,plain,
( ~ sP1
| g_false_only(a,sK3) ),
inference(extension,[status(thm),parent(t29:2)],[f_1_16]) ).
cnf(t32,plain,
$false,
inference(connection,[status(thm),parent(t31:1)],[t31:1,t29:2]) ).
cnf(t33,plain,
$false,
inference(reduction,[status(thm),parent(t31:2)],[t31:2,t13:5]) ).
cnf(t34,plain,
~ g_true_only(sK1(a),sK1(sK1(a))),
inference(extension,[status(thm),parent(t13:6)],[f_1_12]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t13:6]) ).
cnf(t36,plain,
~ g_true_only(a,sK1(a)),
inference(lemma_extension,[status(thm),parent(t13:7)],[l2:1]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t13:7]) ).
cnf(t38,plain,
~ g_true_only(sK6,sK1(sK6)),
inference(extension,[status(thm),parent(t6:4)],[f_1_12]) ).
cnf(t39,plain,
$false,
inference(connection,[status(thm),parent(t38:1)],[t38:1,t6:4]) ).
cnf(t40,plain,
( g_false_only(sK3,sK4)
| ~ sP1 ),
inference(extension,[status(thm),parent(t6:5)],[f_1_17]) ).
cnf(t41,plain,
$false,
inference(connection,[status(thm),parent(t40:1)],[t40:1,t6:5]) ).
cnf(t42,plain,
( ~ g_false_only(a,sK3)
| ~ g_false_only(sK3,sK4) ),
inference(extension,[status(thm),parent(t40:2)],[f_1_11]) ).
cnf(t43,plain,
$false,
inference(connection,[status(thm),parent(t42:1)],[t42:1,t40:2]) ).
cnf(t44,plain,
( ~ sP1
| g_false_only(a,sK3) ),
inference(extension,[status(thm),parent(t42:2)],[f_1_16]) ).
cnf(t45,plain,
$false,
inference(connection,[status(thm),parent(t44:1)],[t44:1,t42:2]) ).
cnf(t46,plain,
$false,
inference(reduction,[status(thm),parent(t44:2)],[t44:2,t6:5]) ).
cnf(t47,plain,
~ g_true_only(sK1(a),sK1(sK1(a))),
inference(extension,[status(thm),parent(t6:6)],[f_1_12]) ).
cnf(t48,plain,
$false,
inference(connection,[status(thm),parent(t47:1)],[t47:1,t6:6]) ).
cnf(t49,plain,
~ g_true_only(a,sK1(a)),
inference(lemma_extension,[status(thm),parent(t6:7)],[l2:1]) ).
cnf(t50,plain,
$false,
inference(connection,[status(thm),parent(t49:1)],[t49:1,t6:7]) ).
cnf(l1,lemma,
g_false_only(a,sK1(a)),
inference(lemma,[status(cth),parent(t1:1),below(0:0)],[t1:1]) ).
cnf(t51,plain,
( g_both(sK1(a),sK1(sK1(a)))
| g_true_only(sK1(a),sK1(sK1(a)))
| g_false_only(sK1(a),sK1(sK1(a))) ),
inference(extension,[status(thm),parent(t1:2)],[f_5_3]) ).
cnf(t52,plain,
$false,
inference(connection,[status(thm),parent(t51:1)],[t51:1,t1:2]) ).
cnf(t53,plain,
~ g_true_only(sK1(a),sK1(sK1(a))),
inference(extension,[status(thm),parent(t51:2)],[f_1_12]) ).
cnf(t54,plain,
$false,
inference(connection,[status(thm),parent(t53:1)],[t53:1,t51:2]) ).
cnf(t55,plain,
( g_true_only(a,sK1(a))
| g_true_only(sK1(a),sK1(sK1(a)))
| sP1
| g_true_only(sK6,sK1(sK6))
| g_false_only(sK1(a),sK5(sK1(a)))
| sP0(sK1(a),sK1(sK1(a)))
| ~ g_both(sK1(a),sK1(sK1(a))) ),
inference(extension,[status(thm),parent(t51:3)],[f_1_13]) ).
cnf(t56,plain,
$false,
inference(connection,[status(thm),parent(t55:1)],[t55:1,t51:3]) ).
cnf(t57,plain,
( ~ g_both(sK1(a),sK1(sK1(a)))
| g_false_only(sK1(a),sK2(sK1(a)))
| ~ sP0(sK1(a),sK1(sK1(a))) ),
inference(extension,[status(thm),parent(t55:2)],[f_1_15]) ).
cnf(t58,plain,
$false,
inference(connection,[status(thm),parent(t57:1)],[t57:1,t55:2]) ).
cnf(t59,plain,
( ~ g_false_only(a,sK1(a))
| ~ g_false_only(sK1(a),sK2(sK1(a))) ),
inference(extension,[status(thm),parent(t57:2)],[f_1_11]) ).
cnf(t60,plain,
$false,
inference(connection,[status(thm),parent(t59:1)],[t59:1,t57:2]) ).
cnf(t61,plain,
( g_both(a,sK1(a))
| g_true_only(a,sK1(a))
| g_false_only(a,sK1(a)) ),
inference(extension,[status(thm),parent(t59:2)],[f_5_3]) ).
cnf(t62,plain,
$false,
inference(connection,[status(thm),parent(t61:1)],[t61:1,t59:2]) ).
cnf(t63,plain,
~ g_true_only(a,sK1(a)),
inference(extension,[status(thm),parent(t61:2)],[f_1_12]) ).
cnf(t64,plain,
$false,
inference(connection,[status(thm),parent(t63:1)],[t63:1,t61:2]) ).
cnf(t65,plain,
( ~ sP0(sK1(a),sK1(sK1(a)))
| ~ g_both(a,sK1(a)) ),
inference(extension,[status(thm),parent(t61:3)],[f_1_14]) ).
cnf(t66,plain,
$false,
inference(connection,[status(thm),parent(t65:1)],[t65:1,t61:3]) ).
cnf(t67,plain,
$false,
inference(reduction,[status(thm),parent(t65:2)],[t65:2,t55:2]) ).
cnf(t68,plain,
$false,
inference(reduction,[status(thm),parent(t57:3)],[t57:3,t51:3]) ).
cnf(t69,plain,
( ~ g_false_only(a,sK1(a))
| ~ g_false_only(sK1(a),sK5(sK1(a))) ),
inference(extension,[status(thm),parent(t55:3)],[f_1_11]) ).
cnf(t70,plain,
$false,
inference(connection,[status(thm),parent(t69:1)],[t69:1,t55:3]) ).
cnf(t71,plain,
g_false_only(a,sK1(a)),
inference(lemma_extension,[status(thm),parent(t69:2)],[l1:1]) ).
cnf(t72,plain,
$false,
inference(connection,[status(thm),parent(t71:1)],[t71:1,t69:2]) ).
cnf(t73,plain,
~ g_true_only(sK6,sK1(sK6)),
inference(extension,[status(thm),parent(t55:4)],[f_1_12]) ).
cnf(t74,plain,
$false,
inference(connection,[status(thm),parent(t73:1)],[t73:1,t55:4]) ).
cnf(t75,plain,
( g_false_only(sK3,sK4)
| ~ sP1 ),
inference(extension,[status(thm),parent(t55:5)],[f_1_17]) ).
cnf(t76,plain,
$false,
inference(connection,[status(thm),parent(t75:1)],[t75:1,t55:5]) ).
cnf(t77,plain,
( ~ g_false_only(a,sK3)
| ~ g_false_only(sK3,sK4) ),
inference(extension,[status(thm),parent(t75:2)],[f_1_11]) ).
cnf(t78,plain,
$false,
inference(connection,[status(thm),parent(t77:1)],[t77:1,t75:2]) ).
cnf(t79,plain,
( ~ sP1
| g_false_only(a,sK3) ),
inference(extension,[status(thm),parent(t77:2)],[f_1_16]) ).
cnf(t80,plain,
$false,
inference(connection,[status(thm),parent(t79:1)],[t79:1,t77:2]) ).
cnf(t81,plain,
$false,
inference(reduction,[status(thm),parent(t79:2)],[t79:2,t55:5]) ).
cnf(t82,plain,
( ~ g_false(sK1(a),sK1(sK1(a)))
| ~ g_true_only(sK1(a),sK1(sK1(a))) ),
inference(extension,[status(thm),parent(t55:6)],[f_2_5]) ).
cnf(t83,plain,
$false,
inference(connection,[status(thm),parent(t82:1)],[t82:1,t55:6]) ).
cnf(t84,plain,
( ~ g_both(sK1(a),sK1(sK1(a)))
| g_false(sK1(a),sK1(sK1(a))) ),
inference(extension,[status(thm),parent(t82:2)],[f_3_5]) ).
cnf(t85,plain,
$false,
inference(connection,[status(thm),parent(t84:1)],[t84:1,t82:2]) ).
cnf(t86,plain,
$false,
inference(reduction,[status(thm),parent(t84:2)],[t84:2,t51:3]) ).
cnf(t87,plain,
( ~ g_false(a,sK1(a))
| ~ g_true_only(a,sK1(a)) ),
inference(extension,[status(thm),parent(t55:7)],[f_2_5]) ).
cnf(t88,plain,
$false,
inference(connection,[status(thm),parent(t87:1)],[t87:1,t55:7]) ).
cnf(t89,plain,
( ~ g_false_only(a,sK1(a))
| g_false(a,sK1(a)) ),
inference(extension,[status(thm),parent(t87:2)],[f_4_4]) ).
cnf(t90,plain,
$false,
inference(connection,[status(thm),parent(t89:1)],[t89:1,t87:2]) ).
cnf(t91,plain,
g_false_only(a,sK1(a)),
inference(lemma_extension,[status(thm),parent(t89:2)],[l1:1]) ).
cnf(t92,plain,
$false,
inference(connection,[status(thm),parent(t91:1)],[t91:1,t89:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYO607+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.01 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.02 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/16.15 % Computer : n012.cluster.edu
% 0.03/16.15 % Model : x86_64 x86_64
% 0.03/16.15 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/16.15 % Memory : 8046.5625MB
% 0.03/16.15 % OS : Linux 6.8.0-71-generic
% 0.03/16.15 % CPULimit : 300
% 0.03/16.15 % WCLimit : 300
% 0.03/16.15 % DateTime : Sun Sep 20 07:42:29 UTC 2026
% 0.03/16.15 % CPUTime :
% 2.50/18.62 % SZS status Theorem for theBenchmark
% 2.50/18.62 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------