%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PUZ033-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n013.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 : Fri Sep 25 02:31:55 PM UTC 2026
% Result : Unsatisfiable 4.14s 0.94s
% Output : Proof 4.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 18
% Syntax : Number of formulae : 187 ( 143 unt; 0 def)
% Number of atoms : 263 ( 135 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 159 ( 83 ~; 76 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 13 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-4 aty)
% Number of variables : 23 ( 2 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f11,hypothesis,
wind_in_east,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c12) ).
fof(f11_nnf,plain,
wind_in_east,
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
wind_in_east,
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(t3,plain,
wind_in_east = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t56,plain,
true = wind_in_east,
inference(orient,[status(thm)],[t3]) ).
cnf(f7,axiom,
( ~ i_feel_rheumatic
| door_is_open
| ~ fire_is_lit
| wind_in_gusts ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c8) ).
fof(f7_nnf,plain,
( ~ i_feel_rheumatic
| door_is_open
| ~ fire_is_lit
| wind_in_gusts ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
( ~ i_feel_rheumatic
| door_is_open
| ~ fire_is_lit
| wind_in_gusts ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( ~ i_feel_rheumatic
| door_is_open
| ~ fire_is_lit
| wind_in_gusts ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t26,plain,
ifeq(fire_is_lit,true,ifeq(i_feel_rheumatic,true,or(wind_in_gusts,door_is_open),true),true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t42,plain,
ifeq(fire_is_lit,true,ifeq(i_feel_rheumatic,true,or(wind_in_gusts,door_is_open),true),true) = true,
inference(orient,[status(thm)],[t26]) ).
cnf(t213,plain,
ifeq(fire_is_lit,wind_in_east,ifeq(i_feel_rheumatic,true,or(wind_in_gusts,door_is_open),true),true) = true,
inference(step,[status(thm)],[t42,t56]) ).
cnf(t214,plain,
ifeq(fire_is_lit,wind_in_east,ifeq(i_feel_rheumatic,wind_in_east,or(wind_in_gusts,door_is_open),true),true) = true,
inference(step,[status(thm)],[t213,t56]) ).
cnf(t215,plain,
ifeq(fire_is_lit,wind_in_east,ifeq(i_feel_rheumatic,wind_in_east,or(wind_in_gusts,door_is_open),wind_in_east),true) = true,
inference(step,[status(thm)],[t214,t56]) ).
cnf(t216,plain,
ifeq(fire_is_lit,wind_in_east,ifeq(i_feel_rheumatic,wind_in_east,or(wind_in_gusts,door_is_open),wind_in_east),wind_in_east) = true,
inference(step,[status(thm)],[t215,t56]) ).
cnf(t217,plain,
ifeq(fire_is_lit,wind_in_east,ifeq(i_feel_rheumatic,wind_in_east,or(wind_in_gusts,door_is_open),wind_in_east),wind_in_east) = wind_in_east,
inference(step,[status(thm)],[t216,t56]) ).
cnf(t77,plain,
ifeq(fire_is_lit,wind_in_east,ifeq(i_feel_rheumatic,wind_in_east,or(wind_in_gusts,door_is_open),wind_in_east),wind_in_east) = wind_in_east,
inference(rw,[status(thm)],[t217]) ).
cnf(f3,axiom,
( fire_is_lit
| ~ i_feel_rheumatic
| ~ cold ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c4) ).
fof(f3_nnf,plain,
( fire_is_lit
| ~ i_feel_rheumatic
| ~ cold ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
( fire_is_lit
| ~ i_feel_rheumatic
| ~ cold ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( fire_is_lit
| ~ i_feel_rheumatic
| ~ cold ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t21,plain,
ifeq(cold,true,ifeq(i_feel_rheumatic,true,fire_is_lit,true),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t38,plain,
ifeq(cold,true,ifeq(i_feel_rheumatic,true,fire_is_lit,true),true) = true,
inference(orient,[status(thm)],[t21]) ).
cnf(t203,plain,
ifeq(cold,wind_in_east,ifeq(i_feel_rheumatic,true,fire_is_lit,true),true) = true,
inference(step,[status(thm)],[t38,t56]) ).
cnf(t204,plain,
ifeq(cold,wind_in_east,ifeq(i_feel_rheumatic,wind_in_east,fire_is_lit,true),true) = true,
inference(step,[status(thm)],[t203,t56]) ).
cnf(t205,plain,
ifeq(cold,wind_in_east,ifeq(i_feel_rheumatic,wind_in_east,fire_is_lit,wind_in_east),true) = true,
inference(step,[status(thm)],[t204,t56]) ).
cnf(t206,plain,
ifeq(cold,wind_in_east,ifeq(i_feel_rheumatic,wind_in_east,fire_is_lit,wind_in_east),wind_in_east) = true,
inference(step,[status(thm)],[t205,t56]) ).
cnf(t207,plain,
ifeq(cold,wind_in_east,ifeq(i_feel_rheumatic,wind_in_east,fire_is_lit,wind_in_east),wind_in_east) = wind_in_east,
inference(step,[status(thm)],[t206,t56]) ).
cnf(t75,plain,
ifeq(cold,wind_in_east,ifeq(i_feel_rheumatic,wind_in_east,fire_is_lit,wind_in_east),wind_in_east) = wind_in_east,
inference(rw,[status(thm)],[t207]) ).
cnf(f0,axiom,
( sunshine
| ~ wind_in_east ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c1) ).
fof(f0_nnf,plain,
( sunshine
| ~ wind_in_east ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
( sunshine
| ~ wind_in_east ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( sunshine
| ~ wind_in_east ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,axiom,
ifeq(wind_in_east,true,sunshine,true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(hi9,axiom,
wind_in_east = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(h0,plain,
sunshine = true,
inference(hyper_resolution,[status(thm)],[hi0,hi9]) ).
cnf(f8,axiom,
( foggy
| ~ sunshine ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c9) ).
fof(f8_nnf,plain,
( foggy
| ~ sunshine ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
( foggy
| ~ sunshine ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( foggy
| ~ sunshine ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(hi7,axiom,
ifeq(sunshine,true,foggy,true) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(h1,plain,
foggy = true,
inference(hyper_resolution,[status(thm)],[hi7,h0]) ).
cnf(f6,axiom,
( window_is_shut
| ~ foggy
| cold
| ~ sunshine ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c7) ).
fof(f6_nnf,plain,
( window_is_shut
| ~ foggy
| cold
| ~ sunshine ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
( window_is_shut
| ~ foggy
| cold
| ~ sunshine ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( window_is_shut
| ~ foggy
| cold
| ~ sunshine ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(hi5,axiom,
ifeq(sunshine,true,ifeq(foggy,true,or(cold,window_is_shut),true),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t9,plain,
or(cold,window_is_shut) = true,
inference(hyper_resolution,[status(thm)],[hi5,h0,h1]) ).
cnf(t47,plain,
or(cold,window_is_shut) = true,
inference(orient,[status(thm)],[t9]) ).
cnf(t175,plain,
or(cold,window_is_shut) = wind_in_east,
inference(step,[status(thm)],[t47,t56]) ).
cnf(t61,plain,
or(cold,window_is_shut) = wind_in_east,
inference(orient,[status(thm)],[t175]) ).
cnf(t7,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t29,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(f12,negated_conjecture,
~ window_is_shut,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_window_is_shut) ).
fof(f12_nnf,plain,
~ window_is_shut,
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
~ window_is_shut,
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
~ window_is_shut,
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t4,plain,
window_is_shut = false,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t82,plain,
false = window_is_shut,
inference(orient,[status(thm)],[t4]) ).
cnf(t225,plain,
or(X1,window_is_shut) = X1,
inference(step,[status(thm)],[t29,t82]) ).
cnf(t87,plain,
or(X1,window_is_shut) = X1,
inference(rw,[status(thm)],[t225]) ).
cnf(t93,plain,
or(X1,window_is_shut) = X1,
inference(orient,[status(thm)],[t87]) ).
cnf(t228,plain,
cold = wind_in_east,
inference(step,[status(thm)],[t61,t93]) ).
cnf(t94,plain,
cold = wind_in_east,
inference(rw,[status(thm)],[t228]) ).
cnf(t95,plain,
cold = wind_in_east,
inference(orient,[status(thm)],[t94]) ).
cnf(t241,plain,
ifeq(wind_in_east,wind_in_east,ifeq(i_feel_rheumatic,wind_in_east,fire_is_lit,wind_in_east),wind_in_east) = wind_in_east,
inference(step,[status(thm)],[t75,t95]) ).
cnf(t12,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t28,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t242,plain,
ifeq(i_feel_rheumatic,wind_in_east,fire_is_lit,wind_in_east) = wind_in_east,
inference(step,[status(thm)],[t241,t28]) ).
cnf(f10,axiom,
( i_feel_rheumatic
| ~ wind_in_east
| ~ foggy ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c11) ).
fof(f10_nnf,plain,
( i_feel_rheumatic
| ~ wind_in_east
| ~ foggy ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
( i_feel_rheumatic
| ~ wind_in_east
| ~ foggy ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( i_feel_rheumatic
| ~ wind_in_east
| ~ foggy ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(hi8,axiom,
ifeq(foggy,true,ifeq(wind_in_east,true,i_feel_rheumatic,true),true) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t1,plain,
true = i_feel_rheumatic,
inference(hyper_resolution,[status(thm)],[hi8,h1,hi9]) ).
cnf(t218,plain,
wind_in_east = i_feel_rheumatic,
inference(step,[status(thm)],[t1,t56]) ).
cnf(t78,plain,
i_feel_rheumatic = wind_in_east,
inference(orient,[status(thm)],[t218]) ).
cnf(t243,plain,
ifeq(wind_in_east,wind_in_east,fire_is_lit,wind_in_east) = wind_in_east,
inference(step,[status(thm)],[t242,t78]) ).
cnf(t244,plain,
fire_is_lit = wind_in_east,
inference(step,[status(thm)],[t243,t28]) ).
cnf(t110,plain,
fire_is_lit = wind_in_east,
inference(orient,[status(thm)],[t244]) ).
cnf(t245,plain,
ifeq(wind_in_east,wind_in_east,ifeq(i_feel_rheumatic,wind_in_east,or(wind_in_gusts,door_is_open),wind_in_east),wind_in_east) = wind_in_east,
inference(step,[status(thm)],[t77,t110]) ).
cnf(t246,plain,
ifeq(i_feel_rheumatic,wind_in_east,or(wind_in_gusts,door_is_open),wind_in_east) = wind_in_east,
inference(step,[status(thm)],[t245,t28]) ).
cnf(t247,plain,
ifeq(wind_in_east,wind_in_east,or(wind_in_gusts,door_is_open),wind_in_east) = wind_in_east,
inference(step,[status(thm)],[t246,t78]) ).
cnf(t248,plain,
or(wind_in_gusts,door_is_open) = wind_in_east,
inference(step,[status(thm)],[t247,t28]) ).
cnf(t19,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t219,plain,
ifeq(not(X1),wind_in_east,X1,false) = false,
inference(step,[status(thm)],[t19,t56]) ).
cnf(t79,plain,
ifeq(not(X1),wind_in_east,X1,false) = false,
inference(orient,[status(thm)],[t219]) ).
cnf(t226,plain,
ifeq(not(X1),wind_in_east,X1,window_is_shut) = false,
inference(step,[status(thm)],[t79,t82]) ).
cnf(t227,plain,
ifeq(not(X1),wind_in_east,X1,window_is_shut) = window_is_shut,
inference(step,[status(thm)],[t226,t82]) ).
cnf(t88,plain,
ifeq(not(X1),wind_in_east,X1,window_is_shut) = window_is_shut,
inference(rw,[status(thm)],[t227]) ).
cnf(t102,plain,
ifeq(not(X1),wind_in_east,X1,window_is_shut) = window_is_shut,
inference(orient,[status(thm)],[t88]) ).
cnf(f9,axiom,
( ~ door_is_open
| ~ neighbor_practices_flute ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c10) ).
fof(f9_nnf,plain,
( ~ door_is_open
| ~ neighbor_practices_flute ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
( ~ door_is_open
| ~ neighbor_practices_flute ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( ~ door_is_open
| ~ neighbor_practices_flute ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t18,plain,
or(not(neighbor_practices_flute),not(door_is_open)) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t46,plain,
or(not(neighbor_practices_flute),not(door_is_open)) = true,
inference(orient,[status(thm)],[t18]) ).
cnf(t173,plain,
or(not(neighbor_practices_flute),not(door_is_open)) = wind_in_east,
inference(step,[status(thm)],[t46,t56]) ).
cnf(t59,plain,
or(not(neighbor_practices_flute),not(door_is_open)) = wind_in_east,
inference(orient,[status(thm)],[t173]) ).
cnf(f1,axiom,
( neighbor_practices_flute
| ~ foggy
| ~ cold ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c2) ).
fof(f1_nnf,plain,
( neighbor_practices_flute
| ~ foggy
| ~ cold ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
( neighbor_practices_flute
| ~ foggy
| ~ cold ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( neighbor_practices_flute
| ~ foggy
| ~ cold ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t20,plain,
ifeq(cold,true,ifeq(foggy,true,neighbor_practices_flute,true),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t37,plain,
ifeq(cold,true,ifeq(foggy,true,neighbor_practices_flute,true),true) = true,
inference(orient,[status(thm)],[t20]) ).
cnf(t0,plain,
true = foggy,
inference(hyper_resolution,[status(thm)],[hi7,h0]) ).
cnf(t50,plain,
foggy = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t166,plain,
ifeq(cold,true,ifeq(true,true,neighbor_practices_flute,true),true) = true,
inference(step,[status(thm)],[t37,t50]) ).
cnf(t167,plain,
ifeq(cold,true,neighbor_practices_flute,true) = true,
inference(step,[status(thm)],[t166,t28]) ).
cnf(t52,plain,
ifeq(cold,true,neighbor_practices_flute,true) = true,
inference(rw,[status(thm)],[t167]) ).
cnf(t229,plain,
ifeq(wind_in_east,true,neighbor_practices_flute,true) = true,
inference(step,[status(thm)],[t52,t95]) ).
cnf(t230,plain,
ifeq(wind_in_east,wind_in_east,neighbor_practices_flute,true) = true,
inference(step,[status(thm)],[t229,t56]) ).
cnf(t231,plain,
neighbor_practices_flute = true,
inference(step,[status(thm)],[t230,t28]) ).
cnf(t232,plain,
neighbor_practices_flute = wind_in_east,
inference(step,[status(thm)],[t231,t56]) ).
cnf(t96,plain,
neighbor_practices_flute = wind_in_east,
inference(orient,[status(thm)],[t232]) ).
cnf(t233,plain,
or(not(wind_in_east),not(door_is_open)) = wind_in_east,
inference(step,[status(thm)],[t59,t96]) ).
cnf(t6,plain,
not(true) = false,
introduced(definition) ).
cnf(t220,plain,
not(wind_in_east) = false,
inference(step,[status(thm)],[t6,t56]) ).
cnf(t80,plain,
not(wind_in_east) = false,
inference(orient,[status(thm)],[t220]) ).
cnf(t221,plain,
not(wind_in_east) = window_is_shut,
inference(step,[status(thm)],[t80,t82]) ).
cnf(t83,plain,
not(wind_in_east) = window_is_shut,
inference(orient,[status(thm)],[t221]) ).
cnf(t234,plain,
or(window_is_shut,not(door_is_open)) = wind_in_east,
inference(step,[status(thm)],[t233,t83]) ).
cnf(t10,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t30,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t10]) ).
cnf(t224,plain,
or(window_is_shut,X1) = X1,
inference(step,[status(thm)],[t30,t82]) ).
cnf(t86,plain,
or(window_is_shut,X1) = X1,
inference(rw,[status(thm)],[t224]) ).
cnf(t92,plain,
or(window_is_shut,X1) = X1,
inference(orient,[status(thm)],[t86]) ).
cnf(t235,plain,
not(door_is_open) = wind_in_east,
inference(step,[status(thm)],[t234,t92]) ).
cnf(t97,plain,
not(door_is_open) = wind_in_east,
inference(rw,[status(thm)],[t235]) ).
cnf(t98,plain,
not(door_is_open) = wind_in_east,
inference(orient,[status(thm)],[t97]) ).
cnf(t103,plain,
window_is_shut = ifeq(wind_in_east,wind_in_east,door_is_open,window_is_shut),
inference(cp,[status(thm)],[t102,t98]) ).
cnf(t237,plain,
window_is_shut = door_is_open,
inference(step,[status(thm)],[t103,t28]) ).
cnf(t105,plain,
door_is_open = window_is_shut,
inference(orient,[status(thm)],[t237]) ).
cnf(t249,plain,
or(wind_in_gusts,window_is_shut) = wind_in_east,
inference(step,[status(thm)],[t248,t105]) ).
cnf(t250,plain,
wind_in_gusts = wind_in_east,
inference(step,[status(thm)],[t249,t93]) ).
cnf(t111,plain,
wind_in_east = wind_in_gusts,
inference(orient,[status(thm)],[t250]) ).
cnf(t255,plain,
true = wind_in_gusts,
inference(step,[status(thm)],[t56,t111]) ).
cnf(t116,plain,
true = wind_in_gusts,
inference(orient,[status(thm)],[t255]) ).
cnf(f2,axiom,
( door_is_open
| ~ fire_smokes ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c3) ).
fof(f2_nnf,plain,
( door_is_open
| ~ fire_smokes ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
( door_is_open
| ~ fire_smokes ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( door_is_open
| ~ fire_smokes ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t13,plain,
ifeq(fire_smokes,true,door_is_open,true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t41,plain,
ifeq(fire_smokes,true,door_is_open,true) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(t187,plain,
ifeq(fire_smokes,wind_in_east,door_is_open,true) = true,
inference(step,[status(thm)],[t41,t56]) ).
cnf(t188,plain,
ifeq(fire_smokes,wind_in_east,door_is_open,wind_in_east) = true,
inference(step,[status(thm)],[t187,t56]) ).
cnf(t189,plain,
ifeq(fire_smokes,wind_in_east,door_is_open,wind_in_east) = wind_in_east,
inference(step,[status(thm)],[t188,t56]) ).
cnf(t71,plain,
ifeq(fire_smokes,wind_in_east,door_is_open,wind_in_east) = wind_in_east,
inference(rw,[status(thm)],[t189]) ).
cnf(t99,plain,
ifeq(fire_smokes,wind_in_east,door_is_open,wind_in_east) = wind_in_east,
inference(orient,[status(thm)],[t71]) ).
cnf(t238,plain,
ifeq(fire_smokes,wind_in_east,window_is_shut,wind_in_east) = wind_in_east,
inference(step,[status(thm)],[t99,t105]) ).
cnf(t106,plain,
ifeq(fire_smokes,wind_in_east,window_is_shut,wind_in_east) = wind_in_east,
inference(rw,[status(thm)],[t238]) ).
cnf(t108,plain,
ifeq(fire_smokes,wind_in_east,window_is_shut,wind_in_east) = wind_in_east,
inference(orient,[status(thm)],[t106]) ).
cnf(t267,plain,
ifeq(fire_smokes,wind_in_gusts,window_is_shut,wind_in_east) = wind_in_east,
inference(step,[status(thm)],[t108,t111]) ).
cnf(t268,plain,
ifeq(fire_smokes,wind_in_gusts,window_is_shut,wind_in_gusts) = wind_in_east,
inference(step,[status(thm)],[t267,t111]) ).
cnf(t269,plain,
ifeq(fire_smokes,wind_in_gusts,window_is_shut,wind_in_gusts) = wind_in_gusts,
inference(step,[status(thm)],[t268,t111]) ).
cnf(t128,plain,
ifeq(fire_smokes,wind_in_gusts,window_is_shut,wind_in_gusts) = wind_in_gusts,
inference(rw,[status(thm)],[t269]) ).
cnf(f4,axiom,
( fire_smokes
| ~ wind_in_gusts
| ~ wind_in_east ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c5) ).
fof(f4_nnf,plain,
( fire_smokes
| ~ wind_in_gusts
| ~ wind_in_east ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
( fire_smokes
| ~ wind_in_gusts
| ~ wind_in_east ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( fire_smokes
| ~ wind_in_gusts
| ~ wind_in_east ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t25,plain,
ifeq(wind_in_east,true,ifeq(wind_in_gusts,true,fire_smokes,true),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t35,plain,
ifeq(wind_in_east,true,ifeq(wind_in_gusts,true,fire_smokes,true),true) = true,
inference(orient,[status(thm)],[t25]) ).
cnf(t208,plain,
ifeq(wind_in_east,wind_in_east,ifeq(wind_in_gusts,true,fire_smokes,true),true) = true,
inference(step,[status(thm)],[t35,t56]) ).
cnf(t209,plain,
ifeq(wind_in_gusts,true,fire_smokes,true) = true,
inference(step,[status(thm)],[t208,t28]) ).
cnf(t210,plain,
ifeq(wind_in_gusts,wind_in_east,fire_smokes,true) = true,
inference(step,[status(thm)],[t209,t56]) ).
cnf(t211,plain,
ifeq(wind_in_gusts,wind_in_east,fire_smokes,wind_in_east) = true,
inference(step,[status(thm)],[t210,t56]) ).
cnf(t212,plain,
ifeq(wind_in_gusts,wind_in_east,fire_smokes,wind_in_east) = wind_in_east,
inference(step,[status(thm)],[t211,t56]) ).
cnf(t76,plain,
ifeq(wind_in_gusts,wind_in_east,fire_smokes,wind_in_east) = wind_in_east,
inference(rw,[status(thm)],[t212]) ).
cnf(t101,plain,
ifeq(wind_in_gusts,wind_in_east,fire_smokes,wind_in_east) = wind_in_east,
inference(orient,[status(thm)],[t76]) ).
cnf(t272,plain,
ifeq(wind_in_gusts,wind_in_gusts,fire_smokes,wind_in_east) = wind_in_east,
inference(step,[status(thm)],[t101,t111]) ).
cnf(t273,plain,
fire_smokes = wind_in_east,
inference(step,[status(thm)],[t272,t28]) ).
cnf(t274,plain,
fire_smokes = wind_in_gusts,
inference(step,[status(thm)],[t273,t111]) ).
cnf(t130,plain,
fire_smokes = wind_in_gusts,
inference(rw,[status(thm)],[t274]) ).
cnf(t137,plain,
fire_smokes = wind_in_gusts,
inference(orient,[status(thm)],[t130]) ).
cnf(t289,plain,
ifeq(wind_in_gusts,wind_in_gusts,window_is_shut,wind_in_gusts) = wind_in_gusts,
inference(step,[status(thm)],[t128,t137]) ).
cnf(t290,plain,
window_is_shut = wind_in_gusts,
inference(step,[status(thm)],[t289,t28]) ).
cnf(t141,plain,
wind_in_gusts = window_is_shut,
inference(orient,[status(thm)],[t290]) ).
cnf(t295,plain,
true = window_is_shut,
inference(step,[status(thm)],[t116,t141]) ).
cnf(t146,plain,
true = window_is_shut,
inference(orient,[status(thm)],[t295]) ).
cnf(f5,axiom,
( ~ headache
| ~ door_is_open ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c6) ).
fof(f5_nnf,plain,
( ~ headache
| ~ door_is_open ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
( ~ headache
| ~ door_is_open ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( ~ headache
| ~ door_is_open ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c5,c9,c12]) ).
cnf(g0_0,plain,
window_is_shut != false,
inference(rw,[status(thm)],[goal_0,t146]) ).
cnf(g0_1,plain,
window_is_shut != window_is_shut,
inference(rw,[status(thm)],[g0_0,t82]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ033-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.37 % Computer : n013.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Thu Sep 24 06:42:54 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 4.14/0.94 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.14/0.94 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------