%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ018-1 : TPTP v9.3.1. Bugfixed v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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 02:00:16 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ018-1 : TPTP v9.3.1. Bugfixed v1.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n001.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 : Mon Sep 21 03:50:43 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.14/0.39 % Refutation found
% 0.14/0.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.39 fof(f1,axiom,(
% 0.14/0.39 (![X]: (( ~ all_on(X)| on(a,X) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f2,axiom,(
% 0.14/0.39 (![X]: (( ~ all_on(X)| on(b,X) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f3,axiom,(
% 0.14/0.39 (![X]: (( ~ all_on(X)| on(c,X) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f6,axiom,(
% 0.14/0.39 consecutive(sunday,monday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f7,axiom,(
% 0.14/0.39 consecutive(monday,tuesday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f8,axiom,(
% 0.14/0.39 consecutive(tuesday,wednesday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f9,axiom,(
% 0.14/0.39 consecutive(wednesday,thursday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f10,axiom,(
% 0.14/0.39 consecutive(thursday,friday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f14,axiom,(
% 0.14/0.39 ~ same_person(a,b) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f15,axiom,(
% 0.14/0.39 ~ same_person(a,c) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f16,axiom,(
% 0.14/0.39 ~ same_person(b,c) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f19,axiom,(
% 0.14/0.39 ~ same_day(sunday,tuesday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f20,axiom,(
% 0.14/0.39 ~ same_day(sunday,wednesday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f21,axiom,(
% 0.14/0.39 ~ same_day(sunday,thursday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f22,axiom,(
% 0.14/0.39 ~ same_day(sunday,friday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f29,axiom,(
% 0.14/0.39 ~ same_day(tuesday,wednesday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f30,axiom,(
% 0.14/0.39 ~ same_day(tuesday,thursday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f31,axiom,(
% 0.14/0.39 ~ same_day(tuesday,friday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f33,axiom,(
% 0.14/0.39 ~ same_day(wednesday,thursday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f39,hypothesis,(
% 0.14/0.39 ( all_on(sunday)| all_on(monday)| all_on(tuesday)| all_on(wednesday)| all_on(thursday)| all_on(friday)| all_on(saturday) ) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f40,hypothesis,(
% 0.14/0.39 (![X,Y,Z,W,U]: (( ~ consecutive(X,Y)| ~ consecutive(Y,Z)| ~ consecutive(Z,W)| ~ on(U,X)| ~ on(U,Y)| ~ on(U,Z) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f41,hypothesis,(
% 0.14/0.39 (![X,Y,Z,W]: (( on(X,Y)| on(X,Z)| on(W,Y)| on(W,Z)| same_person(X,W)| same_day(Y,Z) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f42,hypothesis,(
% 0.14/0.39 ~ on(a,sunday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f43,hypothesis,(
% 0.14/0.39 ~ on(a,tuesday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f44,hypothesis,(
% 0.14/0.39 ~ on(a,thursday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f45,hypothesis,(
% 0.14/0.39 ~ on(b,thursday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f46,hypothesis,(
% 0.14/0.39 ~ on(b,saturday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f47,hypothesis,(
% 0.14/0.39 ~ on(c,sunday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f48,negated_conjecture,(
% 0.14/0.39 ~ all_on(friday) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f49,plain,(
% 0.14/0.39 ![X0]: (~all_on(X0)|on(a,X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/0.39 fof(f50,plain,(
% 0.14/0.39 ![X0]: (~all_on(X0)|on(b,X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f2])).
% 0.14/0.39 fof(f51,plain,(
% 0.14/0.39 ![X0]: (~all_on(X0)|on(c,X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f3])).
% 0.14/0.39 fof(f54,plain,(
% 0.14/0.39 consecutive(sunday,monday)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f6])).
% 0.14/0.39 fof(f55,plain,(
% 0.14/0.39 consecutive(monday,tuesday)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.14/0.40 fof(f56,plain,(
% 0.14/0.40 consecutive(tuesday,wednesday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/0.40 fof(f57,plain,(
% 0.14/0.40 consecutive(wednesday,thursday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f9])).
% 0.14/0.40 fof(f58,plain,(
% 0.14/0.40 consecutive(thursday,friday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f10])).
% 0.14/0.40 fof(f62,plain,(
% 0.14/0.40 ~same_person(a,b)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f14])).
% 0.14/0.40 fof(f63,plain,(
% 0.14/0.40 ~same_person(a,c)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f15])).
% 0.14/0.40 fof(f64,plain,(
% 0.14/0.40 ~same_person(b,c)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f16])).
% 0.14/0.40 fof(f67,plain,(
% 0.14/0.40 ~same_day(sunday,tuesday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f19])).
% 0.14/0.40 fof(f68,plain,(
% 0.14/0.40 ~same_day(sunday,wednesday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f20])).
% 0.14/0.40 fof(f69,plain,(
% 0.14/0.40 ~same_day(sunday,thursday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f21])).
% 0.14/0.40 fof(f70,plain,(
% 0.14/0.40 ~same_day(sunday,friday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f22])).
% 0.14/0.40 fof(f77,plain,(
% 0.14/0.40 ~same_day(tuesday,wednesday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f29])).
% 0.14/0.40 fof(f78,plain,(
% 0.14/0.40 ~same_day(tuesday,thursday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f30])).
% 0.14/0.40 fof(f79,plain,(
% 0.14/0.40 ~same_day(tuesday,friday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f31])).
% 0.14/0.40 fof(f81,plain,(
% 0.14/0.40 ~same_day(wednesday,thursday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f33])).
% 0.14/0.40 fof(f87,plain,(
% 0.14/0.40 all_on(sunday)|all_on(monday)|all_on(tuesday)|all_on(wednesday)|all_on(thursday)|all_on(friday)|all_on(saturday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f39])).
% 0.14/0.40 fof(f88,plain,(
% 0.14/0.40 ![Z,U]: ((![Y]: ((![X]: (((~consecutive(X,Y)|~consecutive(Y,Z))|(![W]: ~consecutive(Z,W)))|~on(U,X)))|~on(U,Y)))|~on(U,Z))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f40])).
% 0.14/0.40 fof(f89,plain,(
% 0.14/0.40 ![X0,X1,X2,X3,X4]: (~consecutive(X0,X1)|~consecutive(X1,X2)|~consecutive(X2,X3)|~on(X4,X0)|~on(X4,X1)|~on(X4,X2))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f88])).
% 0.14/0.40 fof(f90,plain,(
% 0.14/0.40 ![Y,Z]: ((![X,W]: ((((on(X,Y)|on(X,Z))|on(W,Y))|on(W,Z))|same_person(X,W)))|same_day(Y,Z))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f41])).
% 0.14/0.40 fof(f91,plain,(
% 0.14/0.40 ![X0,X1,X2,X3]: (on(X0,X1)|on(X0,X2)|on(X3,X1)|on(X3,X2)|same_person(X0,X3)|same_day(X1,X2))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f90])).
% 0.14/0.40 fof(f92,plain,(
% 0.14/0.40 ~on(a,sunday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.14/0.40 fof(f93,plain,(
% 0.14/0.40 ~on(a,tuesday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f43])).
% 0.14/0.40 fof(f94,plain,(
% 0.14/0.40 ~on(a,thursday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f44])).
% 0.14/0.40 fof(f95,plain,(
% 0.14/0.40 ~on(b,thursday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.40 fof(f96,plain,(
% 0.14/0.40 ~on(b,saturday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f46])).
% 0.14/0.40 fof(f97,plain,(
% 0.14/0.40 ~on(c,sunday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f47])).
% 0.14/0.40 fof(f98,plain,(
% 0.14/0.40 ~all_on(friday)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f48])).
% 0.14/0.40 fof(f99,definition,(
% 0.14/0.40 sQ0_spl <=> (all_on(sunday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f100,plain,(
% 0.14/0.40 all_on(sunday)|~sQ0_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f99])).
% 0.14/0.40 fof(f102,definition,(
% 0.14/0.40 sQ1_spl <=> (all_on(monday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f103,plain,(
% 0.14/0.40 all_on(monday)|~sQ1_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f102])).
% 0.14/0.40 fof(f105,definition,(
% 0.14/0.40 sQ2_spl <=> (all_on(tuesday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f106,plain,(
% 0.14/0.40 all_on(tuesday)|~sQ2_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f105])).
% 0.14/0.40 fof(f108,definition,(
% 0.14/0.40 sQ3_spl <=> (all_on(wednesday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f109,plain,(
% 0.14/0.40 all_on(wednesday)|~sQ3_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f108])).
% 0.14/0.40 fof(f111,definition,(
% 0.14/0.40 sQ4_spl <=> (all_on(thursday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f112,plain,(
% 0.14/0.40 all_on(thursday)|~sQ4_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f111])).
% 0.14/0.40 fof(f114,definition,(
% 0.14/0.40 sQ5_spl <=> (all_on(friday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f115,plain,(
% 0.14/0.40 all_on(friday)|~sQ5_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f114])).
% 0.14/0.40 fof(f117,definition,(
% 0.14/0.40 sQ6_spl <=> (all_on(saturday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f118,plain,(
% 0.14/0.40 all_on(saturday)|~sQ6_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f117])).
% 0.14/0.40 fof(f120,plain,(
% 0.14/0.40 sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl|sQ4_spl|sQ5_spl|sQ6_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f87,f99,f102,f105,f108,f111,f114,f117])).
% 0.14/0.40 fof(f121,plain,(
% 0.14/0.40 on(b,saturday)|~sQ6_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f118,f50])).
% 0.14/0.40 fof(f126,plain,(
% 0.14/0.40 ![X0,X1,X2,X3]: (~consecutive(X0,X1)|~consecutive(X1,X2)|~consecutive(X2,X3)|~on(c,X0)|~on(c,X2)|~all_on(X1))),
% 0.14/0.40 inference(resolution,[status(thm)],[f89,f51])).
% 0.14/0.40 fof(f131,plain,(
% 0.14/0.40 ![X0,X1]: (on(a,X0)|on(X1,tuesday)|on(X1,X0)|same_person(a,X1)|same_day(tuesday,X0))),
% 0.14/0.40 inference(resolution,[status(thm)],[f91,f93])).
% 0.14/0.40 fof(f133,plain,(
% 0.14/0.40 ![X0,X1]: (on(a,X0)|on(X1,sunday)|on(X1,X0)|same_person(a,X1)|same_day(sunday,X0))),
% 0.14/0.40 inference(resolution,[status(thm)],[f91,f92])).
% 0.14/0.40 fof(f143,plain,(
% 0.14/0.40 ![X0,X1]: (on(a,X0)|on(X1,X0)|on(X1,thursday)|same_person(a,X1)|same_day(X0,thursday))),
% 0.14/0.40 inference(resolution,[status(thm)],[f91,f94])).
% 0.14/0.40 fof(f145,plain,(
% 0.14/0.40 ![X0,X1]: (on(a,X0)|on(X1,X0)|on(X1,tuesday)|same_person(a,X1)|same_day(X0,tuesday))),
% 0.14/0.40 inference(resolution,[status(thm)],[f91,f93])).
% 0.14/0.40 fof(f226,definition,(
% 0.14/0.40 sQ13_spl <=> (on(a,thursday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f227,plain,(
% 0.14/0.40 on(a,thursday)|~sQ13_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f226])).
% 0.14/0.40 fof(f230,definition,(
% 0.14/0.40 sQ14_spl <=> (on(a,tuesday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f231,plain,(
% 0.14/0.40 on(a,tuesday)|~sQ14_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f230])).
% 0.14/0.40 fof(f234,definition,(
% 0.14/0.40 sQ15_spl <=> (on(a,sunday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f235,plain,(
% 0.14/0.40 on(a,sunday)|~sQ15_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f234])).
% 0.14/0.40 fof(f238,definition,(
% 0.14/0.40 sQ16_spl <=> (on(b,thursday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f239,plain,(
% 0.14/0.40 on(b,thursday)|~sQ16_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f238])).
% 0.14/0.40 fof(f269,plain,(
% 0.14/0.40 $false|~sQ16_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f239,f95])).
% 0.14/0.40 fof(f270,plain,(
% 0.14/0.40 ~sQ16_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f269])).
% 0.14/0.40 fof(f271,plain,(
% 0.14/0.40 $false|~sQ15_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f235,f92])).
% 0.14/0.40 fof(f272,plain,(
% 0.14/0.40 ~sQ15_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f271])).
% 0.14/0.40 fof(f273,plain,(
% 0.14/0.40 $false|~sQ14_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f231,f93])).
% 0.14/0.40 fof(f274,plain,(
% 0.14/0.40 ~sQ14_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f273])).
% 0.14/0.40 fof(f275,plain,(
% 0.14/0.40 $false|~sQ13_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f227,f94])).
% 0.14/0.40 fof(f276,plain,(
% 0.14/0.40 ~sQ13_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f275])).
% 0.14/0.40 fof(f298,definition,(
% 0.14/0.40 sQ24_spl <=> (on(b,saturday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f299,plain,(
% 0.14/0.40 on(b,saturday)|~sQ24_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f298])).
% 0.14/0.40 fof(f316,plain,(
% 0.14/0.40 $false|~sQ24_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f299,f96])).
% 0.14/0.40 fof(f317,plain,(
% 0.14/0.40 ~sQ24_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f316])).
% 0.14/0.40 fof(f343,plain,(
% 0.14/0.40 $false|~sQ5_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f115,f98])).
% 0.14/0.40 fof(f344,plain,(
% 0.14/0.40 ~sQ5_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f343])).
% 0.14/0.40 fof(f345,plain,(
% 0.14/0.40 sQ24_spl|~sQ6_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f121,f298,f117])).
% 0.14/0.40 fof(f408,definition,(
% 0.14/0.40 sQ43_spl <=> (on(c,thursday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f417,definition,(
% 0.14/0.40 sQ44_spl <=> (on(b,tuesday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f420,definition,(
% 0.14/0.40 sQ45_spl <=> (on(c,tuesday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f426,plain,(
% 0.14/0.40 on(b,thursday)|~sQ4_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f112,f50])).
% 0.14/0.40 fof(f429,plain,(
% 0.14/0.40 sQ16_spl|~sQ4_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f426,f238,f111])).
% 0.14/0.40 fof(f434,plain,(
% 0.14/0.40 ~all_on(sunday)),
% 0.14/0.40 inference(resolution,[status(thm)],[f97,f51])).
% 0.14/0.40 fof(f477,definition,(
% 0.14/0.40 ![X1]: (sQ52_spl <=> (~consecutive(thursday,X1)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f478,plain,(
% 0.14/0.40 ![X0]: (~consecutive(thursday,X0)|~sQ52_spl)),
% 0.14/0.40 inference(component_clause,[status(thm)],[f477])).
% 0.14/0.40 fof(f490,plain,(
% 0.14/0.40 ![X0,X1,X2]: (~consecutive(X0,wednesday)|~consecutive(wednesday,X1)|~consecutive(X1,X2)|~on(c,X0)|~on(c,X1)|~sQ3_spl)),
% 0.14/0.40 inference(resolution,[status(thm)],[f126,f109])).
% 0.14/0.40 fof(f491,definition,(
% 0.14/0.40 ![X0]: (sQ55_spl <=> (~consecutive(X0,wednesday)|~on(c,X0)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f492,plain,(
% 0.14/0.40 ![X0]: (~consecutive(X0,wednesday)|~on(c,X0)|~sQ55_spl)),
% 0.14/0.40 inference(component_clause,[status(thm)],[f491])).
% 0.14/0.40 fof(f494,definition,(
% 0.14/0.40 ![X1,X2]: (sQ56_spl <=> (~consecutive(wednesday,X1)|~consecutive(X1,X2)|~on(c,X1)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f495,plain,(
% 0.14/0.40 ![X0,X1]: (~consecutive(wednesday,X0)|~consecutive(X0,X1)|~on(c,X0)|~sQ56_spl)),
% 0.14/0.40 inference(component_clause,[status(thm)],[f494])).
% 0.14/0.40 fof(f497,plain,(
% 0.14/0.40 sQ55_spl|sQ56_spl|~sQ3_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f490,f491,f494,f108])).
% 0.14/0.40 fof(f500,plain,(
% 0.14/0.40 on(a,tuesday)|~sQ2_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f106,f49])).
% 0.14/0.40 fof(f509,plain,(
% 0.14/0.40 sQ14_spl|~sQ2_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f500,f230,f105])).
% 0.14/0.40 fof(f510,plain,(
% 0.14/0.40 $false|~sQ52_spl),
% 0.14/0.40 inference(backward_subsumption_resolution,[status(thm)],[f58,f478])).
% 0.14/0.40 fof(f511,plain,(
% 0.14/0.40 ~sQ52_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f510])).
% 0.14/0.40 fof(f547,definition,(
% 0.14/0.40 ![X1]: (sQ61_spl <=> (~consecutive(tuesday,X1)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f548,plain,(
% 0.14/0.40 ![X0]: (~consecutive(tuesday,X0)|~sQ61_spl)),
% 0.14/0.40 inference(component_clause,[status(thm)],[f547])).
% 0.14/0.40 fof(f560,plain,(
% 0.14/0.40 $false|~sQ61_spl),
% 0.14/0.40 inference(backward_subsumption_resolution,[status(thm)],[f56,f548])).
% 0.14/0.40 fof(f561,plain,(
% 0.14/0.40 ~sQ61_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f560])).
% 0.14/0.40 fof(f578,definition,(
% 0.14/0.40 sQ64_spl <=> (on(b,sunday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f614,plain,(
% 0.14/0.40 $false|~sQ0_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f100,f434])).
% 0.14/0.40 fof(f615,plain,(
% 0.14/0.40 ~sQ0_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f614])).
% 0.14/0.40 fof(f617,plain,(
% 0.14/0.40 on(b,monday)|~sQ1_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f103,f50])).
% 0.14/0.40 fof(f633,plain,(
% 0.14/0.40 ![X0,X1,X2]: (~consecutive(X0,monday)|~consecutive(monday,X1)|~consecutive(X1,X2)|~on(b,X0)|~on(b,X1)|~sQ1_spl)),
% 0.14/0.40 inference(resolution,[status(thm)],[f617,f89])).
% 0.14/0.40 fof(f641,definition,(
% 0.14/0.40 ![X0]: (sQ75_spl <=> (~consecutive(X0,monday)|~on(b,X0)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f642,plain,(
% 0.14/0.40 ![X0]: (~consecutive(X0,monday)|~on(b,X0)|~sQ75_spl)),
% 0.14/0.40 inference(component_clause,[status(thm)],[f641])).
% 0.14/0.40 fof(f656,definition,(
% 0.14/0.40 ![X1,X2]: (sQ79_spl <=> (~consecutive(monday,X1)|~consecutive(X1,X2)|~on(b,X1)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f657,plain,(
% 0.14/0.40 ![X0,X1]: (~consecutive(monday,X0)|~consecutive(X0,X1)|~on(b,X0)|~sQ79_spl)),
% 0.14/0.40 inference(component_clause,[status(thm)],[f656])).
% 0.14/0.40 fof(f659,plain,(
% 0.14/0.40 sQ75_spl|sQ79_spl|~sQ1_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f633,f641,f656,f102])).
% 0.14/0.40 fof(f750,plain,(
% 0.14/0.40 ~on(b,sunday)|~sQ75_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f642,f54])).
% 0.14/0.40 fof(f764,plain,(
% 0.14/0.40 ~on(c,tuesday)|~sQ55_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f492,f56])).
% 0.14/0.40 fof(f795,definition,(
% 0.14/0.40 sQ85_spl <=> (same_person(a,c))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f796,plain,(
% 0.14/0.40 same_person(a,c)|~sQ85_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f795])).
% 0.14/0.40 fof(f812,definition,(
% 0.14/0.40 sQ89_spl <=> (same_person(a,b))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f813,plain,(
% 0.14/0.40 same_person(a,b)|~sQ89_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f812])).
% 0.14/0.40 fof(f841,plain,(
% 0.14/0.40 $false|~sQ89_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f813,f62])).
% 0.14/0.40 fof(f842,plain,(
% 0.14/0.40 ~sQ89_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f841])).
% 0.14/0.40 fof(f843,plain,(
% 0.14/0.40 $false|~sQ85_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f796,f63])).
% 0.14/0.40 fof(f844,plain,(
% 0.14/0.40 ~sQ85_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f843])).
% 0.14/0.40 fof(f855,plain,(
% 0.14/0.40 on(a,thursday)|on(b,tuesday)|same_person(a,b)|same_day(tuesday,thursday)),
% 0.14/0.40 inference(resolution,[status(thm)],[f131,f95])).
% 0.14/0.40 fof(f871,definition,(
% 0.14/0.40 sQ97_spl <=> (same_day(tuesday,thursday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f872,plain,(
% 0.14/0.40 same_day(tuesday,thursday)|~sQ97_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f871])).
% 0.14/0.40 fof(f881,plain,(
% 0.14/0.40 sQ13_spl|sQ44_spl|sQ89_spl|sQ97_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f855,f226,f417,f812,f871])).
% 0.14/0.40 fof(f913,plain,(
% 0.14/0.40 $false|~sQ97_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f872,f78])).
% 0.14/0.40 fof(f914,plain,(
% 0.14/0.40 ~sQ97_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f913])).
% 0.14/0.40 fof(f922,plain,(
% 0.14/0.40 on(a,thursday)|on(b,sunday)|same_person(a,b)|same_day(sunday,thursday)),
% 0.14/0.40 inference(resolution,[status(thm)],[f133,f95])).
% 0.14/0.40 fof(f937,definition,(
% 0.14/0.40 sQ107_spl <=> (same_day(sunday,thursday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f938,plain,(
% 0.14/0.40 same_day(sunday,thursday)|~sQ107_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f937])).
% 0.14/0.40 fof(f941,definition,(
% 0.14/0.40 sQ108_spl <=> (same_day(sunday,tuesday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f942,plain,(
% 0.14/0.40 same_day(sunday,tuesday)|~sQ108_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f941])).
% 0.14/0.40 fof(f950,plain,(
% 0.14/0.40 sQ13_spl|sQ64_spl|sQ89_spl|sQ107_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f922,f226,f578,f812,f937])).
% 0.14/0.40 fof(f987,plain,(
% 0.14/0.40 $false|~sQ107_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f938,f69])).
% 0.14/0.40 fof(f988,plain,(
% 0.14/0.40 ~sQ107_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f987])).
% 0.14/0.40 fof(f991,plain,(
% 0.14/0.40 $false|~sQ108_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f942,f67])).
% 0.14/0.40 fof(f992,plain,(
% 0.14/0.40 ~sQ108_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f991])).
% 0.14/0.40 fof(f1063,definition,(
% 0.14/0.40 sQ123_spl <=> (same_day(sunday,friday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f1064,plain,(
% 0.14/0.40 same_day(sunday,friday)|~sQ123_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f1063])).
% 0.14/0.40 fof(f1067,definition,(
% 0.14/0.40 sQ124_spl <=> (same_day(tuesday,friday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f1068,plain,(
% 0.14/0.40 same_day(tuesday,friday)|~sQ124_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f1067])).
% 0.14/0.40 fof(f1076,plain,(
% 0.14/0.40 $false|~sQ124_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1068,f79])).
% 0.14/0.40 fof(f1077,plain,(
% 0.14/0.40 ~sQ124_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f1076])).
% 0.14/0.40 fof(f1078,plain,(
% 0.14/0.40 $false|~sQ123_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1064,f70])).
% 0.14/0.40 fof(f1079,plain,(
% 0.14/0.40 ~sQ123_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f1078])).
% 0.14/0.40 fof(f1118,definition,(
% 0.14/0.40 ![X1]: (sQ127_spl <=> (~consecutive(wednesday,X1)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f1119,plain,(
% 0.14/0.40 ![X0]: (~consecutive(wednesday,X0)|~sQ127_spl)),
% 0.14/0.40 inference(component_clause,[status(thm)],[f1118])).
% 0.14/0.40 fof(f1131,plain,(
% 0.14/0.40 $false|~sQ127_spl),
% 0.14/0.40 inference(backward_subsumption_resolution,[status(thm)],[f57,f1119])).
% 0.14/0.40 fof(f1132,plain,(
% 0.14/0.40 ~sQ127_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f1131])).
% 0.14/0.40 fof(f1153,definition,(
% 0.14/0.40 sQ130_spl <=> (same_day(sunday,wednesday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f1154,plain,(
% 0.14/0.40 same_day(sunday,wednesday)|~sQ130_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f1153])).
% 0.14/0.40 fof(f1157,definition,(
% 0.14/0.40 sQ131_spl <=> (same_day(tuesday,wednesday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f1158,plain,(
% 0.14/0.40 same_day(tuesday,wednesday)|~sQ131_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f1157])).
% 0.14/0.40 fof(f1169,plain,(
% 0.14/0.40 $false|~sQ131_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1158,f77])).
% 0.14/0.40 fof(f1170,plain,(
% 0.14/0.40 ~sQ131_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f1169])).
% 0.14/0.40 fof(f1171,plain,(
% 0.14/0.40 $false|~sQ130_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1154,f68])).
% 0.14/0.40 fof(f1172,plain,(
% 0.14/0.40 ~sQ130_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f1171])).
% 0.14/0.40 fof(f1191,definition,(
% 0.14/0.40 sQ134_spl <=> (same_person(b,c))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f1192,plain,(
% 0.14/0.40 same_person(b,c)|~sQ134_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f1191])).
% 0.14/0.40 fof(f1220,plain,(
% 0.14/0.40 $false|~sQ134_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1192,f64])).
% 0.14/0.40 fof(f1221,plain,(
% 0.14/0.40 ~sQ134_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f1220])).
% 0.14/0.40 fof(f1477,plain,(
% 0.14/0.40 on(a,sunday)|on(c,thursday)|same_person(a,c)|same_day(sunday,thursday)),
% 0.14/0.40 inference(resolution,[status(thm)],[f143,f97])).
% 0.14/0.40 fof(f1496,definition,(
% 0.14/0.40 sQ159_spl <=> (same_day(wednesday,thursday))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f1497,plain,(
% 0.14/0.40 same_day(wednesday,thursday)|~sQ159_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f1496])).
% 0.14/0.40 fof(f1500,plain,(
% 0.14/0.40 sQ15_spl|sQ43_spl|sQ85_spl|sQ107_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f1477,f234,f408,f795,f937])).
% 0.14/0.40 fof(f1536,plain,(
% 0.14/0.40 $false|~sQ159_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1497,f81])).
% 0.14/0.40 fof(f1537,plain,(
% 0.14/0.40 ~sQ159_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f1536])).
% 0.14/0.40 fof(f1539,plain,(
% 0.14/0.40 on(a,sunday)|on(c,tuesday)|same_person(a,c)|same_day(sunday,tuesday)),
% 0.14/0.40 inference(resolution,[status(thm)],[f145,f97])).
% 0.14/0.40 fof(f1560,plain,(
% 0.14/0.40 sQ15_spl|sQ45_spl|sQ85_spl|sQ108_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f1539,f234,f420,f795,f941])).
% 0.14/0.40 fof(f1666,plain,(
% 0.14/0.40 ![X0]: (~consecutive(thursday,X0)|~on(c,thursday)|~sQ56_spl)),
% 0.14/0.40 inference(resolution,[status(thm)],[f495,f57])).
% 0.14/0.40 fof(f1667,plain,(
% 0.14/0.40 sQ52_spl|~sQ43_spl|~sQ56_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f1666,f477,f408,f494])).
% 0.14/0.40 fof(f1670,plain,(
% 0.14/0.40 ![X0]: (~consecutive(tuesday,X0)|~on(b,tuesday)|~sQ79_spl)),
% 0.14/0.40 inference(resolution,[status(thm)],[f657,f55])).
% 0.14/0.40 fof(f1671,plain,(
% 0.14/0.40 sQ61_spl|~sQ44_spl|~sQ79_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f1670,f547,f417,f656])).
% 0.14/0.40 fof(f1672,plain,(
% 0.14/0.40 ~sQ64_spl|~sQ75_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f750,f578,f641])).
% 0.14/0.40 fof(f1683,plain,(
% 0.14/0.40 ~sQ45_spl|~sQ55_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f764,f420,f491])).
% 0.14/0.40 fof(f1684,plain,(
% 0.14/0.40 $false),
% 0.14/0.40 inference(sat_refutation,[status(thm)],[f120,f270,f272,f274,f276,f317,f344,f345,f429,f497,f509,f511,f561,f615,f659,f842,f844,f881,f914,f950,f988,f992,f1077,f1079,f1132,f1170,f1172,f1221,f1500,f1537,f1560,f1667,f1671,f1672,f1683])).
% 0.14/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.42 % Elapsed time: 0.048504 seconds
% 0.14/0.42 % CPU time: 0.173385 seconds
% 0.14/0.42 % Total memory used: 8.132 MB
% 0.14/0.42 % Net memory used: 7.919 MB
%------------------------------------------------------------------------------