%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PLA001-1 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n014.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 : Mon Jun 24 13:35:27 EDT 2024 % Result : Unsatisfiable 3.53s 3.66s % Output : CNFRefutation 3.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : PLA001-1 : TPTP v8.2.0. Released v1.0.0. % 0.04/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n014.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Jun 18 16:49:53 EDT 2024 % 0.12/0.34 % CPUTime : % 0.50/0.57 start to proof:theBenchmark % 3.53/3.65 %------------------------------------------- % 3.53/3.65 % File :CSE---1.7 % 3.53/3.65 % Problem :theBenchmark % 3.53/3.65 % Transform :cnf % 3.53/3.65 % Format :tptp:raw % 3.53/3.65 % Command :java -jar mcs_scs.jar %d %s % 3.53/3.65 % 3.53/3.65 % Result :Theorem 3.020000s % 3.53/3.65 % Output :CNFRefutation 3.020000s % 3.53/3.65 %------------------------------------------- % 3.53/3.66 %-------------------------------------------------------------------------- % 3.53/3.66 % File : PLA001-1 : TPTP v8.2.0. Released v1.0.0. % 3.53/3.66 % Domain : Planning % 3.53/3.66 % Problem : Cheyenne to DesMoines, buying a loaf of bread on the way % 3.53/3.66 % Version : Especial. % 3.53/3.66 % English : The problem is to drive from Cheyenne, Wyoming to Des Moines, % 3.53/3.66 % Iowa and end up there with a loaf of bread. A portion of the % 3.53/3.66 % road map is expressed in clause form. The allowable actions % 3.53/3.66 % are to drive from a city to a neighboring city, to buy a loaf % 3.53/3.66 % of bread at a city, and to wait_at at a city for one unit % 3.53/3.66 % of time. Buying a loaf of bread takes one unit of time and % 3.53/3.66 % driving to a neighboring city takes two units of time. % 3.53/3.66 % 3.53/3.66 % Refs : [Pla81] Plaisted (1981), Theorem Proving with Abstraction % 3.53/3.66 % Source : [Pla81] % 3.53/3.66 % Names : - [Pla81] % 3.53/3.66 % 3.53/3.66 % Status : Unsatisfiable % 3.53/3.66 % Rating : 0.09 v8.2.0, 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v6.1.0, 0.21 v6.0.0, 0.33 v5.5.0, 0.25 v5.4.0, 0.28 v5.3.0, 0.35 v5.2.0, 0.23 v5.1.0, 0.19 v5.0.0, 0.13 v4.1.0, 0.20 v4.0.1, 0.14 v3.4.0, 0.00 v3.2.0, 0.33 v3.1.0, 0.00 v2.7.0, 0.12 v2.6.0, 0.14 v2.4.0, 0.14 v2.3.0, 0.14 v2.2.1, 0.22 v2.1.0, 0.00 v2.0.0 % 3.53/3.66 % Syntax : Number of clauses : 16 ( 12 unt; 0 nHn; 16 RR) % 3.53/3.66 % Number of literals : 22 ( 0 equ; 7 neg) % 3.53/3.66 % Maximal clause size : 3 ( 1 avg) % 3.53/3.66 % Maximal term depth : 3 ( 1 avg) % 3.53/3.66 % Number of predicates : 2 ( 2 usr; 0 prp; 2-4 aty) % 3.53/3.66 % Number of functors : 18 ( 18 usr; 14 con; 0-2 aty) % 3.53/3.66 % Number of variables : 20 ( 2 sgn) % 3.53/3.66 % SPC : CNF_UNS_RFO_NEQ_HRN % 3.53/3.66 % 3.53/3.66 % Comments : % 3.53/3.66 %-------------------------------------------------------------------------- % 3.53/3.66 cnf(drive1,axiom, % 3.53/3.66 ( ~ at(FromCity,Loaves,Time,Situation) % 3.53/3.66 | ~ next_to(FromCity,ToCity) % 3.53/3.66 | at(ToCity,Loaves,s(s(Time)),drive(ToCity,Situation)) ) ). % 3.53/3.66 % 3.53/3.66 cnf(drive2,axiom, % 3.53/3.66 ( ~ at(FromCity,Loaves,Time,Situation) % 3.53/3.66 | ~ next_to(ToCity,FromCity) % 3.53/3.66 | at(ToCity,Loaves,s(s(Time)),drive(ToCity,Situation)) ) ). % 3.53/3.66 % 3.53/3.66 cnf(wait_in_city,axiom, % 3.53/3.66 ( ~ at(City,Loaves,Time,Situation) % 3.53/3.66 | at(City,Loaves,s(Time),wait_at(Situation)) ) ). % 3.53/3.66 % 3.53/3.66 cnf(buy_in_city,axiom, % 3.53/3.66 ( ~ at(City,Loaves,Time,Situation) % 3.53/3.66 | at(City,s(Loaves),s(Time),buy(Situation)) ) ). % 3.53/3.66 % 3.53/3.66 cnf(map1,hypothesis, % 3.53/3.66 next_to(winnemucca,elko) ). % 3.53/3.66 % 3.53/3.66 cnf(map2,hypothesis, % 3.53/3.66 next_to(elko,saltLakeCity) ). % 3.53/3.66 % 3.53/3.66 cnf(map3,hypothesis, % 3.53/3.66 next_to(saltLakeCity,rockSprings) ). % 3.53/3.66 % 3.53/3.66 cnf(map4,hypothesis, % 3.53/3.66 next_to(rockSprings,laramie) ). % 3.53/3.66 % 3.53/3.66 cnf(map5,hypothesis, % 3.53/3.66 next_to(laramie,cheyenne) ). % 3.53/3.66 % 3.53/3.66 cnf(map6,hypothesis, % 3.53/3.66 next_to(cheyenne,northPlatte) ). % 3.53/3.66 % 3.53/3.66 cnf(map7,hypothesis, % 3.53/3.66 next_to(northPlatte,grandIsland) ). % 3.53/3.66 % 3.53/3.66 cnf(map8,hypothesis, % 3.53/3.66 next_to(grandIsland,lincoln) ). % 3.53/3.66 % 3.53/3.66 cnf(map9,hypothesis, % 3.53/3.66 next_to(lincoln,omaha) ). % 3.53/3.66 % 3.53/3.66 cnf(map10,hypothesis, % 3.53/3.66 next_to(omaha,desMoines) ). % 3.53/3.66 % 3.53/3.66 cnf(initial,hypothesis, % 3.53/3.66 at(cheyenne,none,start,initial_situation) ). % 3.53/3.66 % 3.53/3.66 cnf(prove_you_gat_get_there_with_bread,negated_conjecture, % 3.53/3.66 ~ at(desMoines,s(none),Time,Situation) ). % 3.53/3.66 % 3.53/3.66 %-------------------------------------------------------------------------- % 3.53/3.66 %------------------------------------------- % 3.53/3.66 % Proof found % 3.53/3.66 % SZS status Theorem for theBenchmark % 3.53/3.66 % SZS output start Proof % 3.53/3.66 %ClaNum:16(EqnAxiom:0) % 3.53/3.66 %VarNum:40(SingletonVarNum:20) % 3.53/3.66 %MaxLitNum:3 % 3.53/3.66 %MaxfuncDepth:2 % 3.53/3.66 %SharedTerms:26 % 3.53/3.66 %goalClause: 12 % 3.53/3.66 %singleGoalClaCount:1 % 3.53/3.66 [1]P1(a1,a2) % 3.53/3.66 [2]P1(a2,a7) % 3.53/3.66 [3]P1(a7,a8) % 3.53/3.66 [4]P1(a8,a9) % 3.53/3.66 [5]P1(a9,a3) % 3.53/3.66 [6]P1(a3,a12) % 3.53/3.66 [7]P1(a12,a10) % 3.53/3.66 [8]P1(a10,a13) % 3.53/3.66 [9]P1(a13,a15) % 3.53/3.66 [10]P1(a15,a5) % 3.53/3.66 [11]P2(a3,a14,a17,a11) % 3.53/3.66 [12]~P2(a5,f16(a14),x121,x122) % 3.53/3.66 [13]~P2(x131,x132,x133,x134)+P2(x131,x132,f16(x133),f18(x134)) % 3.53/3.66 [14]~P2(x141,x142,x143,x144)+P2(x141,f16(x142),f16(x143),f4(x144)) % 3.53/3.66 [15]~P2(x155,x152,x153,x154)+~P1(x151,x155)+P2(x151,x152,f16(f16(x153)),f6(x151,x154)) % 3.53/3.66 [16]~P2(x165,x162,x163,x164)+~P1(x165,x161)+P2(x161,x162,f16(f16(x163)),f6(x161,x164)) % 3.53/3.66 %EqnAxiom % 3.53/3.66 % 3.53/3.66 %------------------------------------------- % 3.60/3.67 cnf(17,plain, % 3.60/3.67 (~P2(a5,a14,x171,x172)), % 3.60/3.67 inference(scs_inference,[],[12,14])). % 3.60/3.67 cnf(18,plain, % 3.60/3.67 (~P2(a5,f16(a14),x181,x182)), % 3.60/3.67 inference(rename_variables,[],[12])). % 3.60/3.67 cnf(22,plain, % 3.60/3.67 (~P2(a15,f16(a14),x221,x222)), % 3.60/3.67 inference(scs_inference,[],[12,18,10,11,14,15,16])). % 3.60/3.67 cnf(9197,plain, % 3.60/3.67 (~P2(a13,f16(a14),x91971,x91972)), % 3.60/3.67 inference(scs_inference,[],[22,17,9,11,15,16])). % 3.60/3.67 cnf(10543,plain, % 3.60/3.67 (~P2(a10,f16(a14),x105431,x105432)), % 3.60/3.68 inference(scs_inference,[],[9197,17,8,11,15,16])). % 3.60/3.68 cnf(11886,plain, % 3.60/3.68 (~P2(a12,f16(a14),x118861,x118862)), % 3.60/3.68 inference(scs_inference,[],[10543,7,16])). % 3.60/3.68 cnf(13238,plain, % 3.60/3.68 ($false), % 3.60/3.68 inference(scs_inference,[],[11886,17,6,11,15,16,14]), % 3.60/3.68 ['proof']). % 3.60/3.68 % SZS output end Proof % 3.60/3.68 % Total time :3.020000s %------------------------------------------------------------------------------