%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LCL109-4 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 07:58:00 AM UTC 2026
% Result : Unsatisfiable 83.38s 17.23s
% Output : CNFRefutation 83.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 57
% Number of leaves : 6
% Syntax : Number of formulae : 145 ( 145 unt; 0 def)
% Number of atoms : 145 ( 144 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 20 ( 20 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 208 ( 15 sgn 10 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(prove_mv_4,axiom,
big_V(implies(x,y),implies(y,x)) != truth,
file('theBenchmark.p',prove_mv_4) ).
cnf(c_3,plain,
big_V(implies(x,y),implies(y,x)) != truth,
inference(clausify,[status(thm)],[prove_mv_4]) ).
fof(big_V_definition,axiom,
! [VAR_0,VAR_1] : big_V(VAR_0,VAR_1) = implies(implies(VAR_0,VAR_1),VAR_1),
file('theBenchmark.p',big_V_definition) ).
cnf(c_5,plain,
big_V(A,B) = implies(implies(A,B),B),
inference(clausify,[status(thm)],[big_V_definition]) ).
fof(wajsberg_4,axiom,
! [VAR_0,VAR_1] : implies(implies(not(VAR_0),not(VAR_1)),implies(VAR_1,VAR_0)) = truth,
file('theBenchmark.p',wajsberg_4) ).
cnf(c_6,plain,
implies(implies(not(A),not(B)),implies(B,A)) = truth,
inference(clausify,[status(thm)],[wajsberg_4]) ).
fof(wajsberg_3,axiom,
! [VAR_0,VAR_1] : implies(implies(VAR_0,VAR_1),VAR_1) = implies(implies(VAR_1,VAR_0),VAR_0),
file('theBenchmark.p',wajsberg_3) ).
cnf(c_7,plain,
implies(implies(A,B),B) = implies(implies(B,A),A),
inference(clausify,[status(thm)],[wajsberg_3]) ).
fof(wajsberg_2,axiom,
! [VAR_0,VAR_1,VAR_2] : implies(implies(VAR_0,VAR_1),implies(implies(VAR_1,VAR_2),implies(VAR_0,VAR_2))) = truth,
file('theBenchmark.p',wajsberg_2) ).
cnf(c_8,plain,
implies(implies(A,B),implies(implies(B,C),implies(A,C))) = truth,
inference(clausify,[status(thm)],[wajsberg_2]) ).
fof(wajsberg_1,axiom,
! [VAR_0] : implies(truth,VAR_0) = VAR_0,
file('theBenchmark.p',wajsberg_1) ).
cnf(c_9,plain,
implies(truth,A) = A,
inference(clausify,[status(thm)],[wajsberg_1]) ).
cnf(c_11,plain,
implies(implies(implies(x,y),implies(y,x)),implies(y,x)) != truth,
inference(paramod,[status(thm)],[c_5,c_3]) ).
cnf(c_13167,plain,
big_V(implies(A,B),B) = implies(implies(implies(B,A),A),B),
inference(paramod,[status(thm)],[c_7,c_5]) ).
cnf(c_13168,plain,
implies(implies(implies(A,B),B),B) = implies(implies(implies(B,A),A),B),
inference(paramod,[status(thm)],[c_5,c_13167]) ).
cnf(c_13169,plain,
implies(implies(B,implies(A,B)),implies(A,B)) = implies(implies(implies(B,A),A),B),
inference(paramod,[status(thm)],[c_7,c_13168]) ).
cnf(c_13,plain,
implies(implies(implies(A,B),B),A) = implies(implies(A,implies(B,A)),implies(B,A)),
inference(copy,[status(thm)],[c_13169]) ).
cnf(c_13170,plain,
implies(truth,implies(A,B)) = implies(implies(implies(A,B),implies(not(B),not(A))),implies(not(B),not(A))),
inference(paramod,[status(thm)],[c_6,c_7]) ).
cnf(c_13171,plain,
implies(A,B) = implies(implies(implies(A,B),implies(not(B),not(A))),implies(not(B),not(A))),
inference(paramod,[status(thm)],[c_9,c_13170]) ).
cnf(c_15,plain,
implies(implies(implies(A,B),implies(not(B),not(A))),implies(not(B),not(A))) = implies(A,B),
inference(copy,[status(thm)],[c_13171]) ).
cnf(c_13172,plain,
implies(truth,implies(implies(implies(A,B),C),implies(implies(not(B),not(A)),C))) = truth,
inference(paramod,[status(thm)],[c_6,c_8]) ).
cnf(c_17,plain,
implies(implies(implies(A,B),C),implies(implies(not(B),not(A)),C)) = truth,
inference(paramod,[status(thm)],[c_9,c_13172]) ).
cnf(c_13173,plain,
implies(truth,implies(implies(A,B),implies(C,B))) = implies(implies(implies(implies(A,B),implies(C,B)),implies(C,A)),implies(C,A)),
inference(paramod,[status(thm)],[c_8,c_7]) ).
cnf(c_13174,plain,
implies(implies(A,B),implies(C,B)) = implies(implies(implies(implies(A,B),implies(C,B)),implies(C,A)),implies(C,A)),
inference(paramod,[status(thm)],[c_9,c_13173]) ).
cnf(c_21,plain,
implies(implies(implies(implies(A,B),implies(C,B)),implies(C,A)),implies(C,A)) = implies(implies(A,B),implies(C,B)),
inference(copy,[status(thm)],[c_13174]) ).
cnf(c_13175,plain,
implies(truth,implies(implies(implies(implies(A,B),implies(C,B)),D),implies(implies(C,A),D))) = truth,
inference(paramod,[status(thm)],[c_8,c_8]) ).
cnf(c_25,plain,
implies(implies(implies(implies(A,B),implies(C,B)),D),implies(implies(C,A),D)) = truth,
inference(paramod,[status(thm)],[c_9,c_13175]) ).
cnf(c_29,plain,
implies(implies(not(A),not(truth)),A) = truth,
inference(paramod,[status(thm)],[c_9,c_6]) ).
cnf(c_13176,plain,
implies(A,A) = implies(implies(A,truth),truth),
inference(paramod,[status(thm)],[c_9,c_7]) ).
cnf(c_30,plain,
implies(implies(A,truth),truth) = implies(A,A),
inference(copy,[status(thm)],[c_13176]) ).
cnf(c_13177,plain,
implies(A,implies(implies(A,B),implies(truth,B))) = truth,
inference(paramod,[status(thm)],[c_9,c_8]) ).
cnf(c_31,plain,
implies(A,implies(implies(A,B),B)) = truth,
inference(paramod,[status(thm)],[c_9,c_13177]) ).
cnf(c_32,plain,
implies(implies(A,truth),implies(B,implies(A,B))) = truth,
inference(paramod,[status(thm)],[c_9,c_8]) ).
cnf(c_13178,plain,
implies(truth,A) = implies(implies(A,implies(not(A),not(truth))),implies(not(A),not(truth))),
inference(paramod,[status(thm)],[c_29,c_7]) ).
cnf(c_13179,plain,
A = implies(implies(A,implies(not(A),not(truth))),implies(not(A),not(truth))),
inference(paramod,[status(thm)],[c_9,c_13178]) ).
cnf(c_55,plain,
implies(implies(A,implies(not(A),not(truth))),implies(not(A),not(truth))) = A,
inference(copy,[status(thm)],[c_13179]) ).
cnf(c_13180,plain,
implies(truth,not(not(truth))) = implies(implies(not(not(truth)),implies(not(truth),not(not(truth)))),implies(not(truth),not(not(truth)))),
inference(paramod,[status(thm)],[c_29,c_13]) ).
cnf(c_13181,plain,
not(not(truth)) = implies(implies(not(not(truth)),implies(not(truth),not(not(truth)))),implies(not(truth),not(not(truth)))),
inference(paramod,[status(thm)],[c_9,c_13180]) ).
cnf(c_79,plain,
implies(implies(not(not(truth)),implies(not(truth),not(not(truth)))),implies(not(truth),not(not(truth)))) = not(not(truth)),
inference(copy,[status(thm)],[c_13181]) ).
cnf(c_13182,plain,
implies(truth,implies(implies(implies(implies(A,B),B),C),implies(A,C))) = truth,
inference(paramod,[status(thm)],[c_31,c_8]) ).
cnf(c_85,plain,
implies(implies(implies(implies(A,B),B),C),implies(A,C)) = truth,
inference(paramod,[status(thm)],[c_9,c_13182]) ).
cnf(c_13183,plain,
truth = implies(implies(truth,A),A),
inference(paramod,[status(thm)],[c_31,c_9]) ).
cnf(c_13184,plain,
truth = implies(A,A),
inference(paramod,[status(thm)],[c_9,c_13183]) ).
cnf(c_88,plain,
implies(A,A) = truth,
inference(copy,[status(thm)],[c_13184]) ).
cnf(c_13185,plain,
implies(A,implies(A,A)) = truth,
inference(paramod,[status(thm)],[c_30,c_31]) ).
cnf(c_90,plain,
implies(A,truth) = truth,
inference(paramod,[status(thm)],[c_88,c_13185]) ).
cnf(c_13186,plain,
implies(truth,implies(B,implies(A,B))) = truth,
inference(paramod,[status(thm)],[c_90,c_32]) ).
cnf(c_92,plain,
implies(A,implies(B,A)) = truth,
inference(paramod,[status(thm)],[c_9,c_13186]) ).
cnf(c_13187,plain,
implies(truth,implies(not(truth),not(not(truth)))) = not(not(truth)),
inference(paramod,[status(thm)],[c_92,c_79]) ).
cnf(c_93,plain,
implies(not(truth),not(not(truth))) = not(not(truth)),
inference(paramod,[status(thm)],[c_9,c_13187]) ).
cnf(c_13188,plain,
implies(implies(implies(A,B),B),A) = implies(truth,implies(B,A)),
inference(paramod,[status(thm)],[c_92,c_13]) ).
cnf(c_98,plain,
implies(implies(implies(A,B),B),A) = implies(B,A),
inference(paramod,[status(thm)],[c_9,c_13188]) ).
cnf(c_13189,plain,
implies(truth,implies(implies(implies(A,B),C),implies(B,C))) = truth,
inference(paramod,[status(thm)],[c_92,c_8]) ).
cnf(c_99,plain,
implies(implies(implies(A,B),C),implies(B,C)) = truth,
inference(paramod,[status(thm)],[c_9,c_13189]) ).
cnf(c_13190,plain,
implies(implies(not(not(truth)),not(not(truth))),not(truth)) = implies(not(not(truth)),not(truth)),
inference(paramod,[status(thm)],[c_93,c_98]) ).
cnf(c_13191,plain,
implies(truth,not(truth)) = implies(not(not(truth)),not(truth)),
inference(paramod,[status(thm)],[c_88,c_13190]) ).
cnf(c_13192,plain,
not(truth) = implies(not(not(truth)),not(truth)),
inference(paramod,[status(thm)],[c_9,c_13191]) ).
cnf(c_113,plain,
implies(not(not(truth)),not(truth)) = not(truth),
inference(copy,[status(thm)],[c_13192]) ).
cnf(c_13193,plain,
implies(truth,implies(not(A),implies(A,B))) = truth,
inference(paramod,[status(thm)],[c_6,c_99]) ).
cnf(c_117,plain,
implies(not(A),implies(A,B)) = truth,
inference(paramod,[status(thm)],[c_9,c_13193]) ).
cnf(c_13194,plain,
implies(truth,implies(implies(implies(A,B),C),implies(implies(implies(D,A),B),C))) = truth,
inference(paramod,[status(thm)],[c_99,c_8]) ).
cnf(c_120,plain,
implies(implies(implies(A,B),C),implies(implies(implies(D,A),B),C)) = truth,
inference(paramod,[status(thm)],[c_9,c_13194]) ).
cnf(c_13195,plain,
implies(truth,implies(not(truth),A)) = truth,
inference(paramod,[status(thm)],[c_29,c_99]) ).
cnf(c_123,plain,
implies(not(truth),A) = truth,
inference(paramod,[status(thm)],[c_9,c_13195]) ).
cnf(c_13196,plain,
implies(implies(implies(A,not(not(truth))),not(truth)),not(truth)) = truth,
inference(paramod,[status(thm)],[c_113,c_99]) ).
cnf(c_13197,plain,
implies(implies(not(truth),implies(A,not(not(truth)))),implies(A,not(not(truth)))) = truth,
inference(paramod,[status(thm)],[c_7,c_13196]) ).
cnf(c_13198,plain,
implies(truth,implies(A,not(not(truth)))) = truth,
inference(paramod,[status(thm)],[c_123,c_13197]) ).
cnf(c_130,plain,
implies(A,not(not(truth))) = truth,
inference(paramod,[status(thm)],[c_9,c_13198]) ).
cnf(c_13199,plain,
truth = not(not(truth)),
inference(paramod,[status(thm)],[c_130,c_93]) ).
cnf(c_131,plain,
not(not(truth)) = truth,
inference(copy,[status(thm)],[c_13199]) ).
cnf(c_13200,plain,
implies(truth,A) = implies(implies(A,not(truth)),not(truth)),
inference(paramod,[status(thm)],[c_123,c_7]) ).
cnf(c_13201,plain,
A = implies(implies(A,not(truth)),not(truth)),
inference(paramod,[status(thm)],[c_9,c_13200]) ).
cnf(c_140,plain,
implies(implies(A,not(truth)),not(truth)) = A,
inference(copy,[status(thm)],[c_13201]) ).
cnf(c_13202,plain,
implies(truth,implies(implies(not(not(truth)),not(not(A))),A)) = truth,
inference(paramod,[status(thm)],[c_29,c_17]) ).
cnf(c_13203,plain,
implies(truth,implies(implies(truth,not(not(A))),A)) = truth,
inference(paramod,[status(thm)],[c_131,c_13202]) ).
cnf(c_13204,plain,
implies(truth,implies(not(not(A)),A)) = truth,
inference(paramod,[status(thm)],[c_9,c_13203]) ).
cnf(c_161,plain,
implies(not(not(A)),A) = truth,
inference(paramod,[status(thm)],[c_9,c_13204]) ).
cnf(c_13205,plain,
implies(truth,implies(A,not(not(A)))) = truth,
inference(paramod,[status(thm)],[c_161,c_6]) ).
cnf(c_172,plain,
implies(A,not(not(A))) = truth,
inference(paramod,[status(thm)],[c_9,c_13205]) ).
cnf(c_13206,plain,
implies(truth,A) = implies(implies(A,not(not(A))),not(not(A))),
inference(paramod,[status(thm)],[c_161,c_7]) ).
cnf(c_13207,plain,
A = implies(implies(A,not(not(A))),not(not(A))),
inference(paramod,[status(thm)],[c_9,c_13206]) ).
cnf(c_13208,plain,
A = implies(truth,not(not(A))),
inference(paramod,[status(thm)],[c_172,c_13207]) ).
cnf(c_13209,plain,
A = not(not(A)),
inference(paramod,[status(thm)],[c_9,c_13208]) ).
cnf(c_173,plain,
not(not(A)) = A,
inference(copy,[status(thm)],[c_13209]) ).
cnf(c_175,plain,
implies(implies(A,not(B)),implies(B,not(A))) = truth,
inference(paramod,[status(thm)],[c_173,c_6]) ).
cnf(c_176,plain,
implies(implies(not(A),B),implies(not(B),A)) = truth,
inference(paramod,[status(thm)],[c_173,c_6]) ).
cnf(c_13210,plain,
implies(implies(implies(A,not(B)),implies(B,not(A))),implies(not(not(B)),not(A))) = implies(A,not(B)),
inference(paramod,[status(thm)],[c_173,c_15]) ).
cnf(c_13211,plain,
implies(truth,implies(not(not(B)),not(A))) = implies(A,not(B)),
inference(paramod,[status(thm)],[c_175,c_13210]) ).
cnf(c_13212,plain,
implies(truth,implies(B,not(A))) = implies(A,not(B)),
inference(paramod,[status(thm)],[c_173,c_13211]) ).
cnf(c_179,plain,
implies(A,not(B)) = implies(B,not(A)),
inference(paramod,[status(thm)],[c_9,c_13212]) ).
cnf(c_13213,plain,
implies(implies(implies(not(A),B),implies(not(B),A)),implies(not(B),not(not(A)))) = implies(not(A),B),
inference(paramod,[status(thm)],[c_173,c_15]) ).
cnf(c_13214,plain,
implies(truth,implies(not(B),not(not(A)))) = implies(not(A),B),
inference(paramod,[status(thm)],[c_176,c_13213]) ).
cnf(c_13215,plain,
implies(truth,implies(not(B),A)) = implies(not(A),B),
inference(paramod,[status(thm)],[c_173,c_13214]) ).
cnf(c_180,plain,
implies(not(A),B) = implies(not(B),A),
inference(paramod,[status(thm)],[c_9,c_13215]) ).
cnf(c_181,plain,
implies(A,implies(not(A),B)) = truth,
inference(paramod,[status(thm)],[c_173,c_117]) ).
cnf(c_13216,plain,
implies(truth,implies(not(A),not(truth))) = A,
inference(paramod,[status(thm)],[c_181,c_55]) ).
cnf(c_184,plain,
implies(not(A),not(truth)) = A,
inference(paramod,[status(thm)],[c_9,c_13216]) ).
cnf(c_13217,plain,
implies(A,not(truth)) = implies(implies(not(truth),not(A)),not(A)),
inference(paramod,[status(thm)],[c_184,c_7]) ).
cnf(c_13218,plain,
implies(A,not(truth)) = implies(truth,not(A)),
inference(paramod,[status(thm)],[c_123,c_13217]) ).
cnf(c_13219,plain,
implies(A,not(truth)) = not(A),
inference(paramod,[status(thm)],[c_9,c_13218]) ).
cnf(c_185,plain,
not(A) = implies(A,not(truth)),
inference(copy,[status(thm)],[c_13219]) ).
cnf(c_13220,plain,
big_V(A,not(truth)) = not(implies(A,not(truth))),
inference(paramod,[status(thm)],[c_185,c_5]) ).
cnf(c_13221,plain,
implies(implies(A,not(truth)),not(truth)) = not(implies(A,not(truth))),
inference(paramod,[status(thm)],[c_5,c_13220]) ).
cnf(c_13222,plain,
A = not(implies(A,not(truth))),
inference(paramod,[status(thm)],[c_140,c_13221]) ).
cnf(c_189,plain,
not(implies(A,not(truth))) = A,
inference(copy,[status(thm)],[c_13222]) ).
cnf(c_191,plain,
implies(implies(not(A),implies(B,not(truth))),implies(B,A)) = truth,
inference(paramod,[status(thm)],[c_185,c_6]) ).
cnf(c_193,plain,
implies(implies(A,B),implies(implies(B,not(truth)),not(A))) = truth,
inference(paramod,[status(thm)],[c_185,c_8]) ).
cnf(c_13223,plain,
implies(implies(implies(A,B),implies(implies(B,not(truth)),not(A))),implies(not(B),not(A))) = implies(A,B),
inference(paramod,[status(thm)],[c_185,c_15]) ).
cnf(c_13224,plain,
implies(truth,implies(not(B),not(A))) = implies(A,B),
inference(paramod,[status(thm)],[c_193,c_13223]) ).
cnf(c_201,plain,
implies(not(A),not(B)) = implies(B,A),
inference(paramod,[status(thm)],[c_9,c_13224]) ).
cnf(c_13225,plain,
implies(implies(implies(not(A),implies(B,not(truth))),implies(B,A)),implies(B,A)) = implies(implies(A,not(truth)),implies(B,not(truth))),
inference(paramod,[status(thm)],[c_185,c_21]) ).
cnf(c_13226,plain,
implies(truth,implies(B,A)) = implies(implies(A,not(truth)),implies(B,not(truth))),
inference(paramod,[status(thm)],[c_191,c_13225]) ).
cnf(c_13227,plain,
implies(B,A) = implies(implies(A,not(truth)),implies(B,not(truth))),
inference(paramod,[status(thm)],[c_9,c_13226]) ).
cnf(c_266,plain,
implies(implies(A,not(truth)),implies(B,not(truth))) = implies(B,A),
inference(copy,[status(thm)],[c_13227]) ).
cnf(c_13228,plain,
implies(A,B) = implies(implies(B,not(truth)),not(A)),
inference(paramod,[status(thm)],[c_189,c_179]) ).
cnf(c_297,plain,
implies(implies(A,not(truth)),not(B)) = implies(B,A),
inference(copy,[status(thm)],[c_13228]) ).
cnf(c_13229,plain,
implies(A,B) = implies(not(B),implies(A,not(truth))),
inference(paramod,[status(thm)],[c_189,c_180]) ).
cnf(c_318,plain,
implies(not(A),implies(B,not(truth))) = implies(B,A),
inference(copy,[status(thm)],[c_13229]) ).
cnf(c_340,plain,
implies(implies(implies(x,y),implies(not(x),not(y))),implies(y,x)) != truth,
inference(paramod,[status(thm)],[c_201,c_11]) ).
cnf(c_420,plain,
implies(implies(implies(x,y),implies(implies(x,not(truth)),not(y))),implies(y,x)) != truth,
inference(paramod,[status(thm)],[c_185,c_340]) ).
cnf(c_537,plain,
implies(implies(implies(x,y),implies(implies(x,not(truth)),implies(y,not(truth)))),implies(y,x)) != truth,
inference(paramod,[status(thm)],[c_185,c_420]) ).
cnf(c_13230,plain,
implies(truth,implies(implies(A,implies(B,C)),implies(B,implies(A,C)))) = truth,
inference(paramod,[status(thm)],[c_85,c_25]) ).
cnf(c_1168,plain,
implies(implies(A,implies(B,C)),implies(B,implies(A,C))) = truth,
inference(paramod,[status(thm)],[c_9,c_13230]) ).
cnf(c_13231,plain,
implies(implies(A,B),implies(A,not(truth))) = implies(implies(implies(A,not(truth)),not(B)),not(B)),
inference(paramod,[status(thm)],[c_318,c_7]) ).
cnf(c_1661,plain,
implies(implies(implies(A,not(truth)),not(B)),not(B)) = implies(implies(A,B),implies(A,not(truth))),
inference(copy,[status(thm)],[c_13231]) ).
cnf(c_2052,plain,
implies(implies(implies(x,y),implies(implies(x,not(truth)),implies(y,not(truth)))),implies(not(x),not(y))) != truth,
inference(paramod,[status(thm)],[c_201,c_537]) ).
cnf(c_10390,plain,
implies(implies(implies(implies(implies(x,not(truth)),implies(y,not(truth))),not(truth)),implies(implies(x,y),not(truth))),implies(not(x),not(y))) != truth,
inference(paramod,[status(thm)],[c_266,c_2052]) ).
cnf(c_13232,plain,
implies(truth,implies(A,implies(B,C))) = implies(implies(implies(A,implies(B,C)),implies(B,implies(A,C))),implies(B,implies(A,C))),
inference(paramod,[status(thm)],[c_1168,c_7]) ).
cnf(c_13233,plain,
implies(A,implies(B,C)) = implies(implies(implies(A,implies(B,C)),implies(B,implies(A,C))),implies(B,implies(A,C))),
inference(paramod,[status(thm)],[c_9,c_13232]) ).
cnf(c_13234,plain,
implies(A,implies(B,C)) = implies(truth,implies(B,implies(A,C))),
inference(paramod,[status(thm)],[c_1168,c_13233]) ).
cnf(c_10426,plain,
implies(A,implies(B,C)) = implies(B,implies(A,C)),
inference(paramod,[status(thm)],[c_9,c_13234]) ).
cnf(c_13235,plain,
implies(implies(implies(implies(y,implies(implies(x,not(truth)),not(truth))),not(truth)),implies(implies(x,y),not(truth))),implies(not(x),not(y))) != truth,
inference(paramod,[status(thm)],[c_10426,c_10390]) ).
cnf(c_13236,plain,
implies(implies(implies(implies(y,x),not(truth)),implies(implies(x,y),not(truth))),implies(not(x),not(y))) != truth,
inference(paramod,[status(thm)],[c_140,c_13235]) ).
cnf(c_13237,plain,
implies(implies(implies(x,y),implies(implies(implies(y,x),not(truth)),not(truth))),implies(not(x),not(y))) != truth,
inference(paramod,[status(thm)],[c_10426,c_13236]) ).
cnf(c_13238,plain,
implies(implies(implies(x,y),implies(y,x)),implies(not(x),not(y))) != truth,
inference(paramod,[status(thm)],[c_140,c_13237]) ).
cnf(c_10547,plain,
implies(implies(y,implies(implies(x,y),x)),implies(not(x),not(y))) != truth,
inference(paramod,[status(thm)],[c_10426,c_13238]) ).
cnf(c_12563,plain,
implies(implies(implies(A,not(truth)),not(B)),not(B)) = implies(A,implies(implies(A,B),not(truth))),
inference(paramod,[status(thm)],[c_10426,c_1661]) ).
cnf(c_13239,plain,
implies(implies(implies(implies(implies(x,y),x),not(truth)),not(y)),implies(not(x),not(y))) != truth,
inference(paramod,[status(thm)],[c_297,c_10547]) ).
cnf(c_13240,plain,
implies(not(x),implies(implies(implies(implies(implies(x,y),x),not(truth)),not(y)),not(y))) != truth,
inference(paramod,[status(thm)],[c_10426,c_13239]) ).
cnf(c_13241,plain,
implies(not(x),implies(implies(implies(x,y),x),implies(implies(implies(implies(x,y),x),y),not(truth)))) != truth,
inference(paramod,[status(thm)],[c_12563,c_13240]) ).
cnf(c_13242,plain,
implies(implies(implies(x,y),x),implies(not(x),implies(implies(implies(implies(x,y),x),y),not(truth)))) != truth,
inference(paramod,[status(thm)],[c_10426,c_13241]) ).
cnf(c_13243,plain,
implies(implies(implies(x,y),x),implies(implies(implies(implies(x,y),x),y),implies(not(x),not(truth)))) != truth,
inference(paramod,[status(thm)],[c_10426,c_13242]) ).
cnf(c_13244,plain,
implies(implies(implies(x,y),x),implies(implies(implies(implies(x,y),x),y),x)) != truth,
inference(paramod,[status(thm)],[c_184,c_13243]) ).
cnf(c_13245,plain,
truth != truth,
inference(paramod,[status(thm)],[c_120,c_13244]) ).
cnf(c_13166,plain,
$false,
inference(copy,[status(thm)],[c_13245]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL109-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/5.65 % Computer : n014.cluster.edu
% 0.18/5.65 % Model : x86_64 x86_64
% 0.18/5.65 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.65 % Memory : 8046.5625MB
% 0.18/5.65 % OS : Linux 6.8.0-71-generic
% 0.18/5.65 % CPULimit : 300
% 0.18/5.65 % WCLimit : 300
% 0.18/5.65 % DateTime : Fri Sep 25 21:51:53 UTC 2026
% 0.18/5.66 % CPUTime :
% 0.18/5.66 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/5.66 % Process 1186903 was started by sandbox on n014,
% 0.18/5.66 % Fri Sep 25 21:51:53 2026
% 0.18/5.66 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.18/5.67
% 0.18/5.67 % From the command line: assign(max_seconds, 300).
% 83.38/17.23
% 83.38/17.23 % SZS status Unsatisfiable for theBenchmark
% 83.38/17.23
% 83.38/17.23 % Proof 1 at 9.87 (+ 1.61) seconds.
% 83.38/17.23 % Length of proof is 60.
% 83.38/17.23 % Level of proof is 23.
% 83.38/17.23 % Maximum clause weight is 27.000.
% 83.38/17.23 % Given clauses 362.
% 83.38/17.23
% 83.38/17.23 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------