%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : PLA001-1 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:01:18 PM UTC 2026
% Result : Unsatisfiable 5.36s 5.63s
% Output : CNFRefutation 5.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 16
% Syntax : Number of clauses : 77 ( 54 unt; 0 nHn; 77 RR)
% Number of literals : 114 ( 0 equ; 68 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-4 aty)
% Number of functors : 18 ( 18 usr; 14 con; 0-2 aty)
% Number of variables : 158 ( 52 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(drive1,axiom,
( at(X5,X2,s(s(X3)),drive(X5,X4))
| ~ at(X1,X2,X3,X4)
| ~ next_to(X1,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',drive1) ).
cnf(drive2,axiom,
( at(X5,X2,s(s(X3)),drive(X5,X4))
| ~ at(X1,X2,X3,X4)
| ~ next_to(X5,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',drive2) ).
cnf(buy_in_city,axiom,
( at(X1,s(X2),s(X3),buy(X4))
| ~ at(X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',buy_in_city) ).
cnf(wait_in_city,axiom,
( at(X1,X2,s(X3),wait_at(X4))
| ~ at(X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wait_in_city) ).
cnf(prove_you_gat_get_there_with_bread,negated_conjecture,
~ at(desMoines,s(none),X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_you_gat_get_there_with_bread) ).
cnf(initial,hypothesis,
at(cheyenne,none,start,initial_situation),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',initial) ).
cnf(map10,hypothesis,
next_to(omaha,desMoines),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map10) ).
cnf(map9,hypothesis,
next_to(lincoln,omaha),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map9) ).
cnf(map8,hypothesis,
next_to(grandIsland,lincoln),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map8) ).
cnf(map7,hypothesis,
next_to(northPlatte,grandIsland),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map7) ).
cnf(map6,hypothesis,
next_to(cheyenne,northPlatte),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map6) ).
cnf(map5,hypothesis,
next_to(laramie,cheyenne),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map5) ).
cnf(map4,hypothesis,
next_to(rockSprings,laramie),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map4) ).
cnf(map3,hypothesis,
next_to(saltLakeCity,rockSprings),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map3) ).
cnf(map2,hypothesis,
next_to(elko,saltLakeCity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map2) ).
cnf(map1,hypothesis,
next_to(winnemucca,elko),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map1) ).
cnf(i_0_16,axiom,
( at(X5,X2,s(s(X3)),drive(X5,X4))
| ~ at(X1,X2,X3,X4)
| ~ next_to(X1,X5) ),
drive1,
[final] ).
cnf(i_0_17,axiom,
( at(X5,X2,s(s(X3)),drive(X5,X4))
| ~ at(X1,X2,X3,X4)
| ~ next_to(X5,X1) ),
drive2,
[final] ).
cnf(i_0_18,axiom,
( at(X1,s(X2),s(X3),buy(X4))
| ~ at(X1,X2,X3,X4) ),
buy_in_city,
[final] ).
cnf(i_0_19,axiom,
( at(X1,X2,s(X3),wait_at(X4))
| ~ at(X1,X2,X3,X4) ),
wait_in_city,
[final] ).
cnf(i_0_20,negated_conjecture,
~ at(desMoines,s(none),X1,X2),
prove_you_gat_get_there_with_bread,
[final] ).
cnf(i_0_21,hypothesis,
at(cheyenne,none,start,initial_situation),
initial,
[final] ).
cnf(i_0_22,hypothesis,
next_to(omaha,desMoines),
map10,
[final] ).
cnf(i_0_23,hypothesis,
next_to(lincoln,omaha),
map9,
[final] ).
cnf(i_0_24,hypothesis,
next_to(grandIsland,lincoln),
map8,
[final] ).
cnf(i_0_25,hypothesis,
next_to(northPlatte,grandIsland),
map7,
[final] ).
cnf(i_0_26,hypothesis,
next_to(cheyenne,northPlatte),
map6,
[final] ).
cnf(i_0_27,hypothesis,
next_to(laramie,cheyenne),
map5,
[final] ).
cnf(i_0_28,hypothesis,
next_to(rockSprings,laramie),
map4,
[final] ).
cnf(i_0_29,hypothesis,
next_to(saltLakeCity,rockSprings),
map3,
[final] ).
cnf(i_0_30,hypothesis,
next_to(elko,saltLakeCity),
map2,
[final] ).
cnf(i_0_31,hypothesis,
next_to(winnemucca,elko),
map1,
[final] ).
cnf(i_0_32,plain,
~ at(desMoines,none,X1,X2),
inference(scs_inference,[],[i_0_20,i_0_18]) ).
cnf(i_0_33,plain,
~ at(desMoines,s(none),X1,X2),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_34,plain,
( at(X1,s(X2),s(X3),buy(X4))
| ~ at(X1,X2,X3,X4) ),
inference(rename_variables,[],[i_0_18]) ).
cnf(i_0_35,plain,
~ at(omaha,s(none),X1,X2),
inference(scs_inference,[],[i_0_20,i_0_33,i_0_22,i_0_18,i_0_16]) ).
cnf(i_0_36,plain,
~ at(desMoines,s(none),X1,X2),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_37,plain,
( at(X1,X2,s(s(X3)),drive(X1,X4))
| ~ next_to(X5,X1)
| ~ at(X5,X2,X3,X4) ),
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_38,plain,
~ next_to(desMoines,cheyenne),
inference(scs_inference,[],[i_0_20,i_0_33,i_0_21,i_0_22,i_0_18,i_0_16,i_0_17]) ).
cnf(i_0_39,plain,
( at(X1,X2,s(s(X3)),drive(X1,X4))
| ~ next_to(X1,X5)
| ~ at(X5,X2,X3,X4) ),
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_40,plain,
~ at(omaha,none,X1,X2),
inference(scs_inference,[],[i_0_35,i_0_18]) ).
cnf(i_0_41,plain,
~ at(omaha,s(none),X1,X2),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_42,plain,
( at(X1,s(X2),s(X3),buy(X4))
| ~ at(X1,X2,X3,X4) ),
inference(rename_variables,[],[i_0_18]) ).
cnf(i_0_43,plain,
~ at(lincoln,s(none),X1,X2),
inference(scs_inference,[],[i_0_35,i_0_41,i_0_23,i_0_18,i_0_16]) ).
cnf(i_0_44,plain,
~ at(omaha,s(none),X1,X2),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_45,plain,
( at(X1,X2,s(s(X3)),drive(X1,X4))
| ~ next_to(X5,X1)
| ~ at(X5,X2,X3,X4) ),
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_46,plain,
~ next_to(desMoines,cheyenne),
inference(scs_inference,[],[i_0_35,i_0_41,i_0_32,i_0_23,i_0_21,i_0_18,i_0_16,i_0_17]) ).
cnf(i_0_47,plain,
~ at(desMoines,none,X1,X2),
inference(rename_variables,[],[i_0_32]) ).
cnf(i_0_48,plain,
( at(X1,X2,s(s(X3)),drive(X1,X4))
| ~ next_to(X1,X5)
| ~ at(X5,X2,X3,X4) ),
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_49,plain,
~ at(lincoln,none,X1,X2),
inference(scs_inference,[],[i_0_43,i_0_18]) ).
cnf(i_0_50,plain,
~ at(lincoln,s(none),X1,X2),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_51,plain,
( at(X1,s(X2),s(X3),buy(X4))
| ~ at(X1,X2,X3,X4) ),
inference(rename_variables,[],[i_0_18]) ).
cnf(i_0_52,plain,
~ at(grandIsland,s(none),X1,X2),
inference(scs_inference,[],[i_0_43,i_0_50,i_0_24,i_0_18,i_0_16]) ).
cnf(i_0_53,plain,
~ at(lincoln,s(none),X1,X2),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_54,plain,
( at(X1,X2,s(s(X3)),drive(X1,X4))
| ~ next_to(X5,X1)
| ~ at(X5,X2,X3,X4) ),
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_55,plain,
~ next_to(desMoines,cheyenne),
inference(scs_inference,[],[i_0_43,i_0_50,i_0_24,i_0_32,i_0_21,i_0_18,i_0_16,i_0_17]) ).
cnf(i_0_56,plain,
~ at(desMoines,none,X1,X2),
inference(rename_variables,[],[i_0_32]) ).
cnf(i_0_57,plain,
( at(X1,X2,s(s(X3)),drive(X1,X4))
| ~ next_to(X1,X5)
| ~ at(X5,X2,X3,X4) ),
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_58,plain,
~ at(grandIsland,none,X1,X2),
inference(scs_inference,[],[i_0_52,i_0_18]) ).
cnf(i_0_59,plain,
~ at(grandIsland,s(none),X1,X2),
inference(rename_variables,[],[i_0_52]) ).
cnf(i_0_60,plain,
( at(X1,s(X2),s(X3),buy(X4))
| ~ at(X1,X2,X3,X4) ),
inference(rename_variables,[],[i_0_18]) ).
cnf(i_0_61,plain,
~ at(northPlatte,s(none),X1,X2),
inference(scs_inference,[],[i_0_52,i_0_59,i_0_25,i_0_18,i_0_16]) ).
cnf(i_0_62,plain,
~ at(grandIsland,s(none),X1,X2),
inference(rename_variables,[],[i_0_52]) ).
cnf(i_0_63,plain,
( at(X1,X2,s(s(X3)),drive(X1,X4))
| ~ next_to(X5,X1)
| ~ at(X5,X2,X3,X4) ),
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_64,plain,
~ next_to(desMoines,cheyenne),
inference(scs_inference,[],[i_0_52,i_0_59,i_0_25,i_0_32,i_0_21,i_0_18,i_0_16,i_0_17]) ).
cnf(i_0_65,plain,
~ at(desMoines,none,X1,X2),
inference(rename_variables,[],[i_0_32]) ).
cnf(i_0_66,plain,
( at(X1,X2,s(s(X3)),drive(X1,X4))
| ~ next_to(X1,X5)
| ~ at(X5,X2,X3,X4) ),
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_67,plain,
~ at(northPlatte,none,X1,X2),
inference(scs_inference,[],[i_0_61,i_0_18]) ).
cnf(i_0_68,plain,
~ at(northPlatte,s(none),X1,X2),
inference(rename_variables,[],[i_0_61]) ).
cnf(i_0_69,plain,
( at(X1,s(X2),s(X3),buy(X4))
| ~ at(X1,X2,X3,X4) ),
inference(rename_variables,[],[i_0_18]) ).
cnf(i_0_70,plain,
~ at(cheyenne,s(none),X1,X2),
inference(scs_inference,[],[i_0_61,i_0_68,i_0_26,i_0_18,i_0_16]) ).
cnf(i_0_71,plain,
~ at(northPlatte,s(none),X1,X2),
inference(rename_variables,[],[i_0_61]) ).
cnf(i_0_72,plain,
( at(X1,X2,s(s(X3)),drive(X1,X4))
| ~ next_to(X5,X1)
| ~ at(X5,X2,X3,X4) ),
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_73,plain,
~ next_to(desMoines,cheyenne),
inference(scs_inference,[],[i_0_61,i_0_68,i_0_26,i_0_32,i_0_21,i_0_18,i_0_16,i_0_17]) ).
cnf(i_0_74,plain,
~ at(desMoines,none,X1,X2),
inference(rename_variables,[],[i_0_32]) ).
cnf(i_0_75,plain,
( at(X1,X2,s(s(X3)),drive(X1,X4))
| ~ next_to(X1,X5)
| ~ at(X5,X2,X3,X4) ),
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_76,plain,
$false,
inference(scs_inference,[],[i_0_70,i_0_21,i_0_18]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PLA001-1 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n007.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 01:25:08 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 5.36/5.63 % Version : CSE_E---1.7
% 5.36/5.63 % Problem : theBenchmark.p
% 5.36/5.63 % SZS status Unsatisfiable for theBenchmark.p
% 5.36/5.63 % SZS output start CNFRefutation
% See solution above
% 5.36/5.69 % Total time : 5.283s
%------------------------------------------------------------------------------