%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX224-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/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 09:16:23 AM UTC 2026
% Result : Unsatisfiable 175.17s 23.66s
% Output : CNFRefutation 175.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 12
% Syntax : Number of formulae : 50 ( 50 unt; 0 def)
% Number of atoms : 50 ( 49 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 13 ( 13 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 6 con; 0-4 aty)
% Number of variables : 113 ( 17 sgn 26 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : aux(VAR_0,VAR_1,VAR_2,just(VAR_3)) = eq(VAR_3,VAR_1),
file('theBenchmark.p',axiom_001) ).
cnf(c_2,plain,
aux(A,B,C,just(D)) = eq(D,B),
inference(clausify,[status(thm)],[axiom_001]) ).
fof(axiom_002,axiom,
notb(btrue) = bfalse,
file('theBenchmark.p',axiom_002) ).
cnf(c_3,plain,
notb(btrue) = bfalse,
inference(clausify,[status(thm)],[axiom_002]) ).
fof(axiom_005,axiom,
! [VAR_0,VAR_1] : index(cons(VAR_0,VAR_1),zero) = just(VAR_0),
file('theBenchmark.p',axiom_005) ).
cnf(c_6,plain,
index(cons(A,B),zero) = just(A),
inference(clausify,[status(thm)],[axiom_005]) ).
fof(axiom_006,axiom,
! [VAR_0,VAR_1,VAR_2] : index(cons(VAR_0,VAR_1),suc(VAR_2)) = index(VAR_1,VAR_2),
file('theBenchmark.p',axiom_006) ).
cnf(c_7,plain,
index(cons(A,B),suc(C)) = index(B,C),
inference(clausify,[status(thm)],[axiom_006]) ).
fof(axiom_007,axiom,
! [VAR_0] : andb(btrue,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_007) ).
cnf(c_8,plain,
andb(btrue,A) = A,
inference(clausify,[status(thm)],[axiom_007]) ).
fof(axiom_009,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : tc(VAR_0,app(VAR_1,VAR_2,VAR_3),VAR_4) = andb(tc(VAR_0,VAR_1,arr(VAR_3,VAR_4)),tc(VAR_0,VAR_2,VAR_3)),
file('theBenchmark.p',axiom_009) ).
cnf(c_10,plain,
tc(A,app(B,C,D),E) = andb(tc(A,B,arr(D,E)),tc(A,C,D)),
inference(clausify,[status(thm)],[axiom_009]) ).
cnf(c_11,plain,
andb(tc(A,B,arr(C,D)),tc(A,E,C)) = tc(A,app(B,E,C),D),
inference(copy,[status(thm)],[c_10]) ).
fof(axiom_010,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : tc(VAR_0,lam(VAR_1),arr(VAR_2,VAR_3)) = tc(cons(VAR_2,VAR_0),VAR_1,VAR_3),
file('theBenchmark.p',axiom_010) ).
cnf(c_12,plain,
tc(A,lam(B),arr(C,D)) = tc(cons(C,A),B,D),
inference(clausify,[status(thm)],[axiom_010]) ).
fof(axiom_014,axiom,
! [VAR_0,VAR_1,VAR_2] : tc(VAR_0,var(VAR_1),VAR_2) = aux(VAR_0,VAR_2,VAR_1,index(VAR_0,VAR_1)),
file('theBenchmark.p',axiom_014) ).
cnf(c_16,plain,
tc(A,var(B),C) = aux(A,C,B,index(A,B)),
inference(clausify,[status(thm)],[axiom_014]) ).
cnf(c_17,plain,
aux(A,B,C,index(A,C)) = tc(A,var(C),B),
inference(copy,[status(thm)],[c_16]) ).
fof(axiom_015,axiom,
! [VAR_0] : sat_synth_w(VAR_0) = notb(tc(nil,VAR_0,arr(arr(a,arr(a,b)),arr(a,b)))),
file('theBenchmark.p',axiom_015) ).
cnf(c_18,plain,
sat_synth_w(A) = notb(tc(nil,A,arr(arr(a,arr(a,b)),arr(a,b)))),
inference(clausify,[status(thm)],[axiom_015]) ).
fof(axiom_046,axiom,
! [VAR_0] : eq(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_046) ).
cnf(c_50,plain,
eq(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_046]) ).
fof(axiom_049,axiom,
! [VAR_0] : eq4(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_049) ).
cnf(c_54,plain,
eq4(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_049]) ).
fof(goal,axiom,
! [VAR_0] : eq4(sat_synth_w(VAR_0),bfalse) != btrue,
file('theBenchmark.p',goal) ).
cnf(c_55,plain,
eq4(sat_synth_w(A),bfalse) != btrue,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_56,plain,
eq4(notb(tc(nil,A,arr(arr(a,arr(a,b)),arr(a,b)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_18,c_55]) ).
cnf(c_17479,plain,
aux(cons(A,B),C,zero,just(A)) = tc(cons(A,B),var(zero),C),
inference(paramod,[status(thm)],[c_6,c_17]) ).
cnf(c_17480,plain,
eq(A,C) = tc(cons(A,B),var(zero),C),
inference(paramod,[status(thm)],[c_2,c_17479]) ).
cnf(c_66,plain,
tc(cons(A,B),var(zero),C) = eq(A,C),
inference(copy,[status(thm)],[c_17480]) ).
cnf(c_67,plain,
aux(cons(A,B),C,suc(D),index(B,D)) = tc(cons(A,B),var(suc(D)),C),
inference(paramod,[status(thm)],[c_7,c_17]) ).
cnf(c_117,plain,
eq4(notb(tc(cons(arr(a,arr(a,b)),nil),A,arr(a,b))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_12,c_56]) ).
cnf(c_139,plain,
eq4(notb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),A,b)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_12,c_117]) ).
cnf(c_155,plain,
andb(tc(cons(A,B),C,arr(D,E)),eq(A,D)) = tc(cons(A,B),app(C,var(zero),D),E),
inference(paramod,[status(thm)],[c_66,c_11]) ).
cnf(c_17481,plain,
aux(cons(A,cons(B,C)),D,suc(zero),just(B)) = tc(cons(A,cons(B,C)),var(suc(zero)),D),
inference(paramod,[status(thm)],[c_6,c_67]) ).
cnf(c_17482,plain,
eq(B,D) = tc(cons(A,cons(B,C)),var(suc(zero)),D),
inference(paramod,[status(thm)],[c_2,c_17481]) ).
cnf(c_292,plain,
tc(cons(A,cons(B,C)),var(suc(zero)),D) = eq(B,D),
inference(copy,[status(thm)],[c_17482]) ).
cnf(c_17483,plain,
andb(tc(cons(A,B),C,arr(A,D)),btrue) = tc(cons(A,B),app(C,var(zero),A),D),
inference(paramod,[status(thm)],[c_50,c_155]) ).
cnf(c_2041,plain,
tc(cons(A,B),app(C,var(zero),A),D) = andb(tc(cons(A,B),C,arr(A,D)),btrue),
inference(copy,[status(thm)],[c_17483]) ).
cnf(c_17484,plain,
andb(eq(A,arr(B,C)),eq(D,B)) = tc(cons(D,cons(A,E)),app(var(suc(zero)),var(zero),B),C),
inference(paramod,[status(thm)],[c_292,c_155]) ).
cnf(c_2064,plain,
tc(cons(A,cons(B,C)),app(var(suc(zero)),var(zero),D),E) = andb(eq(B,arr(D,E)),eq(A,D)),
inference(copy,[status(thm)],[c_17484]) ).
cnf(c_2946,plain,
eq4(notb(andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),A,arr(a,b)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_2041,c_139]) ).
cnf(c_16632,plain,
eq4(notb(andb(andb(eq(arr(a,arr(a,b)),arr(A,arr(a,b))),eq(a,A)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_2064,c_2946]) ).
cnf(c_17485,plain,
eq4(notb(andb(andb(btrue,eq(a,a)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_16632]) ).
cnf(c_17486,plain,
eq4(notb(andb(andb(btrue,btrue),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_17485]) ).
cnf(c_17487,plain,
eq4(notb(andb(btrue,btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_8,c_17486]) ).
cnf(c_17488,plain,
eq4(notb(btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_8,c_17487]) ).
cnf(c_17489,plain,
eq4(bfalse,bfalse) != btrue,
inference(paramod,[status(thm)],[c_3,c_17488]) ).
cnf(c_17490,plain,
btrue != btrue,
inference(paramod,[status(thm)],[c_54,c_17489]) ).
cnf(c_17478,plain,
$false,
inference(copy,[status(thm)],[c_17490]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX224-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.34 % Computer : n010.cluster.edu
% 0.10/0.34 % Model : x86_64 x86_64
% 0.10/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.34 % Memory : 8046.5625MB
% 0.10/0.34 % OS : Linux 6.8.0-71-generic
% 0.10/0.34 % CPULimit : 300
% 0.10/0.34 % WCLimit : 300
% 0.10/0.34 % DateTime : Sat Sep 26 16:59:30 UTC 2026
% 0.10/0.34 % CPUTime :
% 0.10/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.35 % Process 3763056 was started by sandbox2 on n010,
% 0.10/0.35 % Sat Sep 26 16:59:30 2026
% 0.10/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.35
% 0.10/0.35 % From the command line: assign(max_seconds, 300).
% 175.17/23.66
% 175.17/23.66 % given #500 (F,wt=64): 2432 eq4(notb(andb(tc(cons(c,cons(arr(a,arr(a,b)),nil)),A,a),bfalse)),bfalse) != btrue. [para(138(a,1),2154(a,1,1,1))].
% 175.17/23.66
% 175.17/23.66 % given #1000 (T,wt=48): 3168 tc(A,app(app(lam(var(zero)),B,arr(arr(C,D),E)),F,a),V6) = bfalse. [para(2267(a,1),11(a,1,1)),rewrite([9(4)]),flip(a)].
% 175.17/23.66
% 175.17/23.66 % SZS status Unsatisfiable for theBenchmark
% 175.17/23.66
% 175.17/23.66 % Proof 1 at 5.72 (+ 1.31) seconds.
% 175.17/23.66 % Length of proof is 26.
% 175.17/23.66 % Level of proof is 7.
% 175.17/23.66 % Maximum clause weight is 66.000.
% 175.17/23.66 % Given clauses 1227.
% 175.17/23.66
% 175.17/23.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------