%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : COL091-1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 06:57:41 AM UTC 2026
% Result : Unsatisfiable 0.92s 0.69s
% Output : CNFRefutation 0.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 10
% Syntax : Number of formulae : 42 ( 11 unt; 0 def)
% Number of atoms : 115 ( 49 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 107 ( 34 ~; 73 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-3 aty)
% Number of variables : 77 ( 6 sgn 22 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ap_contractE1,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ap_contractE_c4(VAR_0,VAR_1,VAR_2)
| ap_contractE_c3(VAR_0,VAR_1,VAR_2)
| ap_contractE_c2(VAR_0,VAR_1,VAR_2)
| ap_contractE_c1(VAR_0,VAR_1,VAR_2)
| ~ member(pair(comb_app(VAR_0,VAR_1),VAR_2),contract) ),
file('theBenchmark.p',ap_contractE1) ).
cnf(c_2,plain,
( ap_contractE_c4(A,B,C)
| ap_contractE_c3(A,B,C)
| ap_contractE_c2(A,B,C)
| ap_contractE_c1(A,B,C)
| ~ member(pair(comb_app(A,B),C),contract) ),
inference(clausify,[status(thm)],[ap_contractE1]) ).
fof(ap_contractE4,axiom,
! [VAR_0,VAR_1,VAR_2] :
( VAR_0 = comb_app(combK,VAR_2)
| ~ ap_contractE_c1(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',ap_contractE4) ).
cnf(c_4,plain,
( A = comb_app(combK,C)
| ~ ap_contractE_c1(A,B,C) ),
inference(clausify,[status(thm)],[ap_contractE4]) ).
fof(ap_contractE9,axiom,
! [VAR_0,VAR_1,VAR_2] :
( VAR_0 = comb_app(comb_app(combS,ap_contractE_sk1p(VAR_0,VAR_1,VAR_2)),ap_contractE_sk1q(VAR_0,VAR_1,VAR_2))
| ~ ap_contractE_c2(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',ap_contractE9) ).
cnf(c_5,plain,
( A = comb_app(comb_app(combS,ap_contractE_sk1p(A,B,C)),ap_contractE_sk1q(A,B,C))
| ~ ap_contractE_c2(A,B,C) ),
inference(clausify,[status(thm)],[ap_contractE9]) ).
cnf(c_8,plain,
( ap_contractE_c4(A,C,B)
| ap_contractE_c3(A,C,B)
| ap_contractE_c2(A,C,B)
| ~ member(pair(comb_app(A,C),B),contract)
| A = comb_app(combK,B) ),
inference(resolve,[status(thm)],[c_4,c_2]) ).
fof(ap_contractE10,axiom,
! [VAR_0,VAR_1,VAR_2] :
( member(pair(VAR_0,ap_contractE_sk2q(VAR_0,VAR_1,VAR_2)),contract)
| ~ ap_contractE_c3(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',ap_contractE10) ).
cnf(c_13,plain,
( member(pair(A,ap_contractE_sk2q(A,B,C)),contract)
| ~ ap_contractE_c3(A,B,C) ),
inference(clausify,[status(thm)],[ap_contractE10]) ).
cnf(c_16,plain,
( ap_contractE_c4(A,B,C)
| ap_contractE_c3(A,B,C)
| ~ member(pair(comb_app(A,B),C),contract)
| A = comb_app(combK,C)
| A = comb_app(comb_app(combS,ap_contractE_sk1p(A,B,C)),ap_contractE_sk1q(A,B,C)) ),
inference(resolve,[status(thm)],[c_5,c_8]) ).
fof(ap_contractE15,axiom,
! [VAR_0,VAR_1,VAR_2] :
( VAR_2 = comb_app(VAR_0,ap_contractE_sk3q(VAR_0,VAR_1,VAR_2))
| ~ ap_contractE_c4(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',ap_contractE15) ).
cnf(c_28,plain,
( C = comb_app(A,ap_contractE_sk3q(A,B,C))
| ~ ap_contractE_c4(A,B,C) ),
inference(clausify,[status(thm)],[ap_contractE15]) ).
cnf(c_31,plain,
( ap_contractE_c4(A,B,C)
| ~ member(pair(comb_app(A,B),C),contract)
| A = comb_app(combK,C)
| A = comb_app(comb_app(combS,ap_contractE_sk1p(A,B,C)),ap_contractE_sk1q(A,B,C))
| member(pair(A,ap_contractE_sk2q(A,B,C)),contract) ),
inference(resolve,[status(thm)],[c_13,c_16]) ).
fof(ap_contractE13,axiom,
! [VAR_0,VAR_1,VAR_2] :
( member(pair(VAR_1,ap_contractE_sk3q(VAR_0,VAR_1,VAR_2)),contract)
| ~ ap_contractE_c4(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',ap_contractE13) ).
cnf(c_56,plain,
( member(pair(B,ap_contractE_sk3q(A,B,C)),contract)
| ~ ap_contractE_c4(A,B,C) ),
inference(clausify,[status(thm)],[ap_contractE13]) ).
cnf(c_92,plain,
( ~ member(pair(comb_app(B,A),C),contract)
| B = comb_app(combK,C)
| B = comb_app(comb_app(combS,ap_contractE_sk1p(B,A,C)),ap_contractE_sk1q(B,A,C))
| member(pair(B,ap_contractE_sk2q(B,A,C)),contract)
| member(pair(A,ap_contractE_sk3q(B,A,C)),contract) ),
inference(resolve,[status(thm)],[c_56,c_31]) ).
cnf(c_433,plain,
( ~ member(pair(comb_app(B,A),C),contract)
| B = comb_app(combK,C)
| comb_app(comb_app(combS,ap_contractE_sk1p(B,A,C)),ap_contractE_sk1q(B,A,C)) = B
| member(pair(B,ap_contractE_sk2q(B,A,C)),contract)
| member(pair(A,ap_contractE_sk3q(B,A,C)),contract) ),
inference(copy,[status(thm)],[c_92]) ).
cnf(c_93,plain,
( ~ member(pair(comb_app(B,A),C),contract)
| comb_app(combK,C) = B
| comb_app(comb_app(combS,ap_contractE_sk1p(B,A,C)),ap_contractE_sk1q(B,A,C)) = B
| member(pair(B,ap_contractE_sk2q(B,A,C)),contract)
| member(pair(A,ap_contractE_sk3q(B,A,C)),contract) ),
inference(copy,[status(thm)],[c_433]) ).
cnf(c_175,plain,
( ~ member(pair(comb_app(B,C),A),contract)
| B = comb_app(combK,A)
| B = comb_app(comb_app(combS,ap_contractE_sk1p(B,C,A)),ap_contractE_sk1q(B,C,A))
| member(pair(B,ap_contractE_sk2q(B,C,A)),contract)
| A = comb_app(B,ap_contractE_sk3q(B,C,A)) ),
inference(resolve,[status(thm)],[c_28,c_31]) ).
cnf(c_434,plain,
( ~ member(pair(comb_app(B,C),A),contract)
| B = comb_app(combK,A)
| B = comb_app(comb_app(combS,ap_contractE_sk1p(B,C,A)),ap_contractE_sk1q(B,C,A))
| member(pair(B,ap_contractE_sk2q(B,C,A)),contract)
| comb_app(B,ap_contractE_sk3q(B,C,A)) = A ),
inference(copy,[status(thm)],[c_175]) ).
cnf(c_435,plain,
( ~ member(pair(comb_app(B,C),A),contract)
| B = comb_app(combK,A)
| comb_app(comb_app(combS,ap_contractE_sk1p(B,C,A)),ap_contractE_sk1q(B,C,A)) = B
| member(pair(B,ap_contractE_sk2q(B,C,A)),contract)
| comb_app(B,ap_contractE_sk3q(B,C,A)) = A ),
inference(copy,[status(thm)],[c_434]) ).
cnf(c_176,plain,
( ~ member(pair(comb_app(A,B),C),contract)
| comb_app(combK,C) = A
| comb_app(comb_app(combS,ap_contractE_sk1p(A,B,C)),ap_contractE_sk1q(A,B,C)) = A
| member(pair(A,ap_contractE_sk2q(A,B,C)),contract)
| comb_app(A,ap_contractE_sk3q(A,B,C)) = C ),
inference(copy,[status(thm)],[c_435]) ).
fof(k_app,axiom,
! [VAR_0,VAR_1] : combK != comb_app(VAR_0,VAR_1),
file('theBenchmark.p',k_app) ).
cnf(c_182,plain,
combK != comb_app(A,B),
inference(clausify,[status(thm)],[k_app]) ).
cnf(c_183,plain,
comb_app(A,B) != combK,
inference(copy,[status(thm)],[c_182]) ).
fof(k_contractE,axiom,
! [VAR_0] : ~ member(pair(combK,VAR_0),contract),
file('theBenchmark.p',k_contractE) ).
cnf(c_197,plain,
~ member(pair(combK,A),contract),
inference(clausify,[status(thm)],[k_contractE]) ).
fof(k1_contractD_h1,axiom,
member(pair(comb_app(combK,p),r),contract),
file('theBenchmark.p',k1_contractD_h1) ).
cnf(c_199,plain,
member(pair(comb_app(combK,p),r),contract),
inference(clausify,[status(thm)],[k1_contractD_h1]) ).
fof(k1_contractD_c1,axiom,
! [VAR_0] :
( ~ member(pair(p,VAR_0),contract)
| r != comb_app(combK,VAR_0) ),
file('theBenchmark.p',k1_contractD_c1) ).
cnf(c_200,plain,
( ~ member(pair(p,A),contract)
| r != comb_app(combK,A) ),
inference(clausify,[status(thm)],[k1_contractD_c1]) ).
cnf(c_201,plain,
( ~ member(pair(p,A),contract)
| comb_app(combK,A) != r ),
inference(copy,[status(thm)],[c_200]) ).
cnf(c_436,plain,
( comb_app(combK,r) = combK
| comb_app(comb_app(combS,ap_contractE_sk1p(combK,p,r)),ap_contractE_sk1q(combK,p,r)) = combK
| member(pair(combK,ap_contractE_sk2q(combK,p,r)),contract)
| comb_app(combK,ap_contractE_sk3q(combK,p,r)) = r ),
inference(resolve,[status(thm)],[c_199,c_176]) ).
cnf(c_437,plain,
( comb_app(combK,r) = combK
| comb_app(comb_app(combS,ap_contractE_sk1p(combK,p,r)),ap_contractE_sk1q(combK,p,r)) = combK
| comb_app(combK,ap_contractE_sk3q(combK,p,r)) = r ),
inference(resolve,[status(thm)],[c_197,c_436]) ).
cnf(c_438,plain,
( comb_app(combK,r) = combK
| comb_app(combK,ap_contractE_sk3q(combK,p,r)) = r ),
inference(resolve,[status(thm)],[c_183,c_437]) ).
cnf(c_245,plain,
comb_app(combK,ap_contractE_sk3q(combK,p,r)) = r,
inference(resolve,[status(thm)],[c_183,c_438]) ).
cnf(c_439,plain,
( comb_app(combK,r) = combK
| comb_app(comb_app(combS,ap_contractE_sk1p(combK,p,r)),ap_contractE_sk1q(combK,p,r)) = combK
| member(pair(combK,ap_contractE_sk2q(combK,p,r)),contract)
| member(pair(p,ap_contractE_sk3q(combK,p,r)),contract) ),
inference(resolve,[status(thm)],[c_199,c_93]) ).
cnf(c_440,plain,
( comb_app(combK,r) = combK
| comb_app(comb_app(combS,ap_contractE_sk1p(combK,p,r)),ap_contractE_sk1q(combK,p,r)) = combK
| member(pair(p,ap_contractE_sk3q(combK,p,r)),contract) ),
inference(resolve,[status(thm)],[c_197,c_439]) ).
cnf(c_441,plain,
( comb_app(combK,r) = combK
| member(pair(p,ap_contractE_sk3q(combK,p,r)),contract) ),
inference(resolve,[status(thm)],[c_183,c_440]) ).
cnf(c_247,plain,
member(pair(p,ap_contractE_sk3q(combK,p,r)),contract),
inference(resolve,[status(thm)],[c_183,c_441]) ).
cnf(c_442,plain,
~ member(pair(p,ap_contractE_sk3q(combK,p,r)),contract),
inference(resolve,[status(thm)],[c_245,c_201]) ).
cnf(c_432,plain,
$false,
inference(resolve,[status(thm)],[c_247,c_442]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : COL091-1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n010.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Sat Sep 26 23:13:45 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.44 % Process 278389 was started by sandbox on n010,
% 0.16/0.44 % Sat Sep 26 23:13:45 2026
% 0.16/0.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.16/0.44
% 0.16/0.44 % From the command line: assign(max_seconds, 300).
% 0.92/0.69
% 0.92/0.69 % SZS status Unsatisfiable for theBenchmark
% 0.92/0.69
% 0.92/0.69 % Proof 1 at 0.20 (+ 0.04) seconds.
% 0.92/0.69 % Length of proof is 22.
% 0.92/0.69 % Level of proof is 7.
% 0.92/0.69 % Maximum clause weight is 51.000.
% 0.92/0.69 % Given clauses 116.
% 0.92/0.69
% 0.92/0.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------