%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SWX222+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:09:07 AM UTC 2026
% Result : Theorem 192.59s 207.76s
% Output : Proof 192.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 7
% Syntax : Number of formulae : 45 ( 20 unt; 0 def)
% Number of atoms : 91 ( 19 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 83 ( 37 ~; 32 |; 10 &)
% ( 3 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 64 ( 2 sgn 48 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_026,axiom,
! [E] :
( nf(lam(E))
<=> nf(E) ),
file('theBenchmark.p',axiom_026) ).
fof(axiom_027,axiom,
! [X4] : nf(var(X4)),
file('theBenchmark.p',axiom_027) ).
fof(axiom_029,axiom,
! [Z,Xs] : index(cons(Z,Xs),zero) = just(Z),
file('theBenchmark.p',axiom_029) ).
fof(axiom_033,axiom,
! [X,E,Tx2,T1] :
( tc(X,lam(E),arr(Tx2,T1))
<=> tc(cons(Tx2,X),E,T1) ),
file('theBenchmark.p',axiom_033) ).
fof(axiom_035,axiom,
! [X,Z,X3,Tx3] :
( index(X,X3) = just(Tx3)
=> ( tc(X,var(X3),Z)
<=> Tx3 = Z ) ),
file('theBenchmark.p',axiom_035) ).
fof(goal_036,conjecture,
? [E] :
( tc(nil,E,arr(a,arr(b,b)))
& nf(E) ),
file('theBenchmark.p',goal_036) ).
fof(f_26_1,plain,
! [E] :
( ( nf(lam(E))
| ~ nf(E) )
& ( nf(E)
| ~ nf(lam(E)) ) ),
inference(fof_nnf,[status(thm)],[axiom_026]) ).
fof(f_26_2,plain,
! [U_51] :
( ( nf(lam(U_51))
| ~ nf(U_51) )
& ( nf(U_51)
| ~ nf(lam(U_51)) ) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_3,plain,
( ! [U_53] :
( nf(lam(U_53))
| ~ nf(U_53) )
& ! [U_52] :
( nf(U_52)
| ~ nf(lam(U_52)) ) ),
inference(miniscope,[status(thm)],[f_26_2]) ).
cnf(f_26_5,plain,
( nf(lam(U_53))
| ~ nf(U_53) ),
inference(clausify,[status(thm)],[f_26_3]) ).
fof(f_27_1,plain,
! [X4] : nf(var(X4)),
inference(fof_nnf,[status(thm)],[axiom_027]) ).
fof(f_27_2,plain,
! [U_54] : nf(var(U_54)),
inference(variable_rename,[status(thm)],[f_27_1]) ).
cnf(f_27_3,plain,
nf(var(U_54)),
inference(clausify,[status(thm)],[f_27_2]) ).
fof(f_29_1,plain,
! [Z,Xs] : index(cons(Z,Xs),zero) = just(Z),
inference(fof_nnf,[status(thm)],[axiom_029]) ).
fof(f_29_2,plain,
! [U_57,U_56] : index(cons(U_57,U_56),zero) = just(U_57),
inference(variable_rename,[status(thm)],[f_29_1]) ).
cnf(f_29_3,plain,
index(cons(U_57,U_56),zero) = just(U_57),
inference(clausify,[status(thm)],[f_29_2]) ).
fof(f_33_1,plain,
! [X,E,Tx2,T1] :
( ( tc(X,lam(E),arr(Tx2,T1))
| ~ tc(cons(Tx2,X),E,T1) )
& ( tc(cons(Tx2,X),E,T1)
| ~ tc(X,lam(E),arr(Tx2,T1)) ) ),
inference(fof_nnf,[status(thm)],[axiom_033]) ).
fof(f_33_2,plain,
! [U_82,U_81,U_80,U_79] :
( ( tc(U_82,lam(U_81),arr(U_80,U_79))
| ~ tc(cons(U_80,U_82),U_81,U_79) )
& ( tc(cons(U_80,U_82),U_81,U_79)
| ~ tc(U_82,lam(U_81),arr(U_80,U_79)) ) ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
fof(f_33_3,plain,
( ! [U_90,U_88,U_86,U_84] :
( tc(U_90,lam(U_88),arr(U_86,U_84))
| ~ tc(cons(U_86,U_90),U_88,U_84) )
& ! [U_89,U_87,U_85,U_83] :
( tc(cons(U_85,U_89),U_87,U_83)
| ~ tc(U_89,lam(U_87),arr(U_85,U_83)) ) ),
inference(miniscope,[status(thm)],[f_33_2]) ).
cnf(f_33_5,plain,
( tc(U_90,lam(U_88),arr(U_86,U_84))
| ~ tc(cons(U_86,U_90),U_88,U_84) ),
inference(clausify,[status(thm)],[f_33_3]) ).
fof(f_35_1,plain,
! [X,Z,X3,Tx3] :
( ( ( tc(X,var(X3),Z)
| Tx3 != Z )
& ( Tx3 = Z
| ~ tc(X,var(X3),Z) ) )
| index(X,X3) != just(Tx3) ),
inference(fof_nnf,[status(thm)],[axiom_035]) ).
fof(f_35_2,plain,
! [U_97,U_96,U_95,U_94] :
( ( ( tc(U_97,var(U_95),U_96)
| U_94 != U_96 )
& ( U_94 = U_96
| ~ tc(U_97,var(U_95),U_96) ) )
| index(U_97,U_95) != just(U_94) ),
inference(variable_rename,[status(thm)],[f_35_1]) ).
cnf(f_35_4,plain,
( tc(U_97,var(U_95),U_96)
| U_94 != U_96
| index(U_97,U_95) != just(U_94) ),
inference(clausify,[status(thm)],[f_35_2]) ).
fof(f_36_1,negated_conjecture,
~ ? [E] :
( tc(nil,E,arr(a,arr(b,b)))
& nf(E) ),
inference(negate,[status(cth)],[goal_036]) ).
fof(f_36_2,negated_conjecture,
! [E] :
( ~ tc(nil,E,arr(a,arr(b,b)))
| ~ nf(E) ),
inference(fof_nnf,[status(thm)],[f_36_1]) ).
fof(f_36_3,negated_conjecture,
! [U_98] :
( ~ tc(nil,U_98,arr(a,arr(b,b)))
| ~ nf(U_98) ),
inference(variable_rename,[status(thm)],[f_36_2]) ).
cnf(f_36_4,negated_conjecture,
( ~ tc(nil,U_98,arr(a,arr(b,b)))
| ~ nf(U_98) ),
inference(clausify,[status(thm)],[f_36_3]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(t1,plain,
( ~ nf(lam(lam(var(zero))))
| ~ tc(nil,lam(lam(var(zero))),arr(a,arr(b,b))) ),
inference(start,[status(thm),parent(0:0)],[f_36_4]) ).
cnf(t2,plain,
( ~ tc(cons(a,nil),lam(var(zero)),arr(b,b))
| tc(nil,lam(lam(var(zero))),arr(a,arr(b,b))) ),
inference(extension,[status(thm),parent(t1:1)],[f_33_5]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ tc(cons(b,cons(a,nil)),var(zero),b)
| tc(cons(a,nil),lam(var(zero)),arr(b,b)) ),
inference(extension,[status(thm),parent(t2:2)],[f_33_5]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( b != b
| index(cons(b,cons(a,nil)),zero) != just(b)
| tc(cons(b,cons(a,nil)),var(zero),b) ),
inference(extension,[status(thm),parent(t4:2)],[f_35_4]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
index(cons(b,cons(a,nil)),zero) = just(b),
inference(extension,[status(thm),parent(t6:2)],[f_29_3]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
b = b,
inference(extension,[status(thm),parent(t6:3)],[equality_1]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t6:3]) ).
cnf(t12,plain,
( ~ nf(lam(var(zero)))
| nf(lam(lam(var(zero)))) ),
inference(extension,[status(thm),parent(t1:2)],[f_26_5]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t1:2]) ).
cnf(t14,plain,
( ~ nf(var(zero))
| nf(lam(var(zero))) ),
inference(extension,[status(thm),parent(t12:2)],[f_26_5]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(t16,plain,
nf(var(zero)),
inference(extension,[status(thm),parent(t14:2)],[f_27_3]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t14:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX222+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/15.42 % CPULimit : 300
% 0.07/15.42 % WCLimit : 300
% 0.07/15.42 % DateTime : Sun Sep 20 06:17:58 UTC 2026
% 0.07/15.42 % CPUTime :
% 192.59/207.76 % SZS status Theorem for theBenchmark
% 192.59/207.76 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------