%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : COL089-1 : TPTP v9.3.1. Released v2.7.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 : 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 : Thu Sep 24 08:14:32 AM UTC 2026
% Result : Unsatisfiable 9.96s 10.20s
% Output : Proof 10.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(k_s,axiom,
combK != combS,
file('theBenchmark.p',k_s) ).
cnf(k_app,axiom,
combK != comb_app(P,Q),
file('theBenchmark.p',k_app) ).
cnf(s_app,axiom,
combS != comb_app(P,Q),
file('theBenchmark.p',s_app) ).
cnf(app_app1,axiom,
( P1 = P2
| comb_app(P1,Q1) != comb_app(P2,Q2) ),
file('theBenchmark.p',app_app1) ).
cnf(app_app2,axiom,
( Q1 = Q2
| comb_app(P1,Q1) != comb_app(P2,Q2) ),
file('theBenchmark.p',app_app2) ).
cnf(app_app3,axiom,
( comb_app(P1,Q1) = comb_app(P2,Q2)
| Q1 != Q2
| P1 != P2 ),
file('theBenchmark.p',app_app3) ).
cnf(ap_E1,axiom,
( member(P,comb)
| ~ member(comb_app(P,Q),comb) ),
file('theBenchmark.p',ap_E1) ).
cnf(ap_E2,axiom,
( member(Q,comb)
| ~ member(comb_app(P,Q),comb) ),
file('theBenchmark.p',ap_E2) ).
cnf(comb_intros1,axiom,
member(combK,comb),
file('theBenchmark.p',comb_intros1) ).
cnf(comb_intros2,axiom,
member(combS,comb),
file('theBenchmark.p',comb_intros2) ).
cnf(comb_intros3,axiom,
( member(comb_app(P,Q),comb)
| ~ member(Q,comb)
| ~ member(P,comb) ),
file('theBenchmark.p',comb_intros3) ).
cnf(reduction_refl,axiom,
( member(pair(A,A),rtrancl(contract))
| ~ member(A,comb) ),
file('theBenchmark.p',reduction_refl) ).
cnf(contract_K,axiom,
( member(pair(comb_app(comb_app(combK,P),Q),P),contract)
| ~ member(Q,comb)
| ~ member(P,comb) ),
file('theBenchmark.p',contract_K) ).
cnf(contract_S,axiom,
( member(pair(comb_app(comb_app(comb_app(combS,P),Q),R),comb_app(comb_app(P,R),comb_app(Q,R))),contract)
| ~ member(R,comb)
| ~ member(Q,comb)
| ~ member(P,comb) ),
file('theBenchmark.p',contract_S) ).
cnf(ap_contractE1,axiom,
( ap_contractE_c4(P,Q,R)
| ap_contractE_c3(P,Q,R)
| ap_contractE_c2(P,Q,R)
| ap_contractE_c1(P,Q,R)
| ~ member(pair(comb_app(P,Q),R),contract) ),
file('theBenchmark.p',ap_contractE1) ).
cnf(ap_contractE2,axiom,
( member(R,comb)
| ~ ap_contractE_c1(P,Q,R) ),
file('theBenchmark.p',ap_contractE2) ).
cnf(ap_contractE3,axiom,
( member(Q,comb)
| ~ ap_contractE_c1(P,Q,R) ),
file('theBenchmark.p',ap_contractE3) ).
cnf(ap_contractE4,axiom,
( P = comb_app(combK,R)
| ~ ap_contractE_c1(P,Q,R) ),
file('theBenchmark.p',ap_contractE4) ).
cnf(ap_contractE5,axiom,
( member(ap_contractE_sk1p(P,Q,R),comb)
| ~ ap_contractE_c2(P,Q,R) ),
file('theBenchmark.p',ap_contractE5) ).
cnf(ap_contractE6,axiom,
( member(ap_contractE_sk1q(P,Q,R),comb)
| ~ ap_contractE_c2(P,Q,R) ),
file('theBenchmark.p',ap_contractE6) ).
cnf(ap_contractE7,axiom,
( member(Q,comb)
| ~ ap_contractE_c2(P,Q,R) ),
file('theBenchmark.p',ap_contractE7) ).
cnf(ap_contractE8,axiom,
( R = comb_app(comb_app(ap_contractE_sk1p(P,Q,R),Q),comb_app(ap_contractE_sk1q(P,Q,R),Q))
| ~ ap_contractE_c2(P,Q,R) ),
file('theBenchmark.p',ap_contractE8) ).
cnf(ap_contractE9,axiom,
( P = comb_app(comb_app(combS,ap_contractE_sk1p(P,Q,R)),ap_contractE_sk1q(P,Q,R))
| ~ ap_contractE_c2(P,Q,R) ),
file('theBenchmark.p',ap_contractE9) ).
cnf(ap_contractE10,axiom,
( member(pair(P,ap_contractE_sk2q(P,Q,R)),contract)
| ~ ap_contractE_c3(P,Q,R) ),
file('theBenchmark.p',ap_contractE10) ).
cnf(ap_contractE11,axiom,
( member(Q,comb)
| ~ ap_contractE_c3(P,Q,R) ),
file('theBenchmark.p',ap_contractE11) ).
cnf(ap_contractE12,axiom,
( R = comb_app(ap_contractE_sk2q(P,Q,R),Q)
| ~ ap_contractE_c3(P,Q,R) ),
file('theBenchmark.p',ap_contractE12) ).
cnf(ap_contractE13,axiom,
( member(pair(Q,ap_contractE_sk3q(P,Q,R)),contract)
| ~ ap_contractE_c4(P,Q,R) ),
file('theBenchmark.p',ap_contractE13) ).
cnf(ap_contractE14,axiom,
( member(P,comb)
| ~ ap_contractE_c4(P,Q,R) ),
file('theBenchmark.p',ap_contractE14) ).
cnf(ap_contractE15,axiom,
( R = comb_app(P,ap_contractE_sk3q(P,Q,R))
| ~ ap_contractE_c4(P,Q,R) ),
file('theBenchmark.p',ap_contractE15) ).
cnf(k_contractE,axiom,
~ member(pair(combK,R),contract),
file('theBenchmark.p',k_contractE) ).
cnf(s_contractE,axiom,
~ member(pair(combS,R),contract),
file('theBenchmark.p',s_contractE) ).
cnf(reduction_rls_1,axiom,
( member(pair(comb_app(comb_app(combK,B),Q3),C),rtrancl(contract))
| ~ member(pair(B,C),rtrancl(contract))
| ~ member(Q3,comb)
| ~ member(B,comb) ),
file('theBenchmark.p',reduction_rls_1) ).
cnf(reduction_rls_2,axiom,
( member(pair(comb_app(comb_app(comb_app(combS,P3),Q3),R3),C),rtrancl(contract))
| ~ member(pair(comb_app(comb_app(P3,R3),comb_app(Q3,R3)),C),rtrancl(contract))
| ~ member(R3,comb)
| ~ member(Q3,comb)
| ~ member(P3,comb) ),
file('theBenchmark.p',reduction_rls_2) ).
cnf(reduction_rls_3,axiom,
( member(pair(comb_app(P3,R3),C),rtrancl(contract))
| ~ member(pair(comb_app(Q3,R3),C),rtrancl(contract))
| ~ member(R3,comb)
| ~ member(pair(P3,Q3),contract) ),
file('theBenchmark.p',reduction_rls_3) ).
cnf(reduction_rls_4,axiom,
( member(pair(comb_app(R3,P3),C),rtrancl(contract))
| ~ member(pair(comb_app(R3,Q3),C),rtrancl(contract))
| ~ member(R3,comb)
| ~ member(pair(P3,Q3),contract) ),
file('theBenchmark.p',reduction_rls_4) ).
cnf(trans_rtrancl,axiom,
trans(rtrancl(R)),
file('theBenchmark.p',trans_rtrancl) ).
cnf(transD,axiom,
( member(pair(A,C),R)
| ~ member(pair(B,C),R)
| ~ member(pair(A,B),R)
| ~ trans(R) ),
file('theBenchmark.p',transD) ).
cnf(contract_combD2,axiom,
( member(B,comb)
| ~ member(pair(A,B),contract) ),
file('theBenchmark.p',contract_combD2) ).
cnf(ap_reduce2_2h1,hypothesis,
member(r,comb),
file('theBenchmark.p',ap_reduce2_2h1) ).
cnf(ap_reduce2_2h2,hypothesis,
member(p,comb),
file('theBenchmark.p',ap_reduce2_2h2) ).
cnf(ap_reduce2_2h3,hypothesis,
member(pair(p,y),rtrancl(contract)),
file('theBenchmark.p',ap_reduce2_2h3) ).
cnf(ap_reduce2_2h4,hypothesis,
member(pair(y,z),contract),
file('theBenchmark.p',ap_reduce2_2h4) ).
cnf(ap_reduce2_2h5,hypothesis,
member(pair(comb_app(r,p),comb_app(r,y)),rtrancl(contract)),
file('theBenchmark.p',ap_reduce2_2h5) ).
cnf(ap_reduce2_2c1,negated_conjecture,
~ member(pair(comb_app(r,p),comb_app(r,z)),rtrancl(contract)),
file('theBenchmark.p',ap_reduce2_2c1) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( comb_app(Eq_x_0,Eq_x_1) = comb_app(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( pair(Eq_x_0,Eq_x_1) = pair(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( rtrancl(Eq_x_0) = rtrancl(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( ap_contractE_sk1p(Eq_x_0,Eq_x_1,Eq_x_2) = ap_contractE_sk1p(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( ap_contractE_sk1q(Eq_x_0,Eq_x_1,Eq_x_2) = ap_contractE_sk1q(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( ap_contractE_sk2q(Eq_x_0,Eq_x_1,Eq_x_2) = ap_contractE_sk2q(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( ap_contractE_sk3q(Eq_x_0,Eq_x_1,Eq_x_2) = ap_contractE_sk3q(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( member(Eq_y_0,Eq_y_1)
| ~ member(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_12,axiom,
( ap_contractE_c1(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ ap_contractE_c1(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_13,axiom,
( ap_contractE_c2(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ ap_contractE_c2(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_14,axiom,
( ap_contractE_c3(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ ap_contractE_c3(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,axiom,
( ap_contractE_c4(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ ap_contractE_c4(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_16,axiom,
( trans(Eq_y_0)
| ~ trans(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COL089-1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 This is a CNF_UNS_RFO_SEQ_NHN 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.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 : Sun Sep 20 15:00:21 UTC 2026
% 0.09/0.37 % CPUTime :
% 9.96/10.20 % SZS status Unsatisfiable for theBenchmark
% 9.96/10.20 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------