%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PLA002-2 : 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 : n019.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 241.74s 241.86s % Output : CNFRefutation 243.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PLA002-2 : TPTP v8.2.0. Released v1.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n019.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Tue Jun 18 16:50:38 EDT 2024 % 0.12/0.33 % CPUTime : % 0.50/0.55 start to proof:theBenchmark % 241.73/241.80 %------------------------------------------- % 241.73/241.80 % File :CSE---1.7 % 241.73/241.80 % Problem :theBenchmark % 241.73/241.80 % Transform :cnf % 241.73/241.80 % Format :tptp:raw % 241.73/241.80 % Command :java -jar mcs_scs.jar %d %s % 241.73/241.80 % 241.73/241.80 % Result :Theorem 241.080000s % 241.73/241.80 % Output :CNFRefutation 241.080000s % 241.73/241.80 %------------------------------------------- % 241.74/241.86 %-------------------------------------------------------------------------- % 241.74/241.86 % File : PLA002-2 : TPTP v8.2.0. Released v1.0.0. % 241.74/241.86 % Domain : Planning % 241.74/241.86 % Problem : Getting from here to there, in all weather % 241.74/241.86 % Version : Especial. % 241.74/241.86 % Theorem formulation : Augmented. % 241.74/241.86 % English : % 241.74/241.86 % 241.74/241.86 % Refs : [Pla82] Plaisted (1982), A Simplified Problem Reduction Format % 241.74/241.86 % Source : [TPTP] % 241.74/241.86 % Names : % 241.74/241.86 % 241.74/241.86 % Status : Unsatisfiable % 241.74/241.86 % Rating : 0.00 v7.4.0, 0.17 v7.1.0, 0.33 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.12 v5.4.0, 0.20 v5.2.0, 0.10 v5.1.0, 0.18 v5.0.0, 0.14 v4.1.0, 0.12 v4.0.1, 0.00 v2.4.0, 0.00 v2.2.1, 0.25 v2.1.0, 0.50 v2.0.0 % 241.74/241.86 % Syntax : Number of clauses : 23 ( 2 unt; 1 nHn; 18 RR) % 241.74/241.86 % Number of literals : 64 ( 0 equ; 41 neg) % 241.74/241.86 % Maximal clause size : 4 ( 2 avg) % 241.74/241.86 % Maximal term depth : 2 ( 1 avg) % 241.74/241.86 % Number of predicates : 4 ( 4 usr; 0 prp; 1-2 aty) % 241.74/241.86 % Number of functors : 12 ( 12 usr; 7 con; 0-2 aty) % 241.74/241.86 % Number of variables : 27 ( 5 sgn) % 241.74/241.86 % SPC : CNF_UNS_RFO_NEQ_NHN % 241.74/241.86 % 241.74/241.86 % Comments : Includes sort information in the clauses. Inspired by the % 241.74/241.86 % problems of building a model if there is no sort info. in the % 241.74/241.86 % clauses. In this case the natural interpretation is not a % 241.74/241.86 % model of the hypotheses, as meaningless (FALSE) instances of % 241.74/241.86 % clauses can be made. % 241.74/241.86 % : Modified by Geoff Sutcliffe. % 241.74/241.86 %-------------------------------------------------------------------------- % 241.74/241.86 cnf(warm_or_cold,hypothesis, % 241.74/241.86 ( warm(Situation1) % 241.74/241.86 | cold(Situation2) % 241.74/241.86 | ~ situation(Situation1) % 241.74/241.86 | ~ situation(Situation2) ) ). % 241.74/241.86 % 241.74/241.86 cnf(walk_a_to_b,hypothesis, % 241.74/241.86 ( ~ at(a,Situation) % 241.74/241.86 | at(b,walk(b,Situation)) % 241.74/241.86 | ~ situation(Situation) ) ). % 241.74/241.86 % 241.74/241.86 cnf(drive_a_to_b,hypothesis, % 241.74/241.86 ( ~ at(a,Situation) % 241.74/241.86 | at(b,drive(b,Situation)) % 241.74/241.86 | ~ situation(Situation) ) ). % 241.74/241.86 % 241.74/241.86 cnf(walk_b_to_a,hypothesis, % 241.74/241.86 ( ~ at(b,Situation) % 241.74/241.86 | at(a,walk(a,Situation)) % 241.74/241.86 | ~ situation(Situation) ) ). % 241.74/241.86 % 241.74/241.86 cnf(drive_b_to_a,hypothesis, % 241.74/241.86 ( ~ at(b,Situation) % 241.74/241.86 | at(a,drive(a,Situation)) % 241.74/241.86 | ~ situation(Situation) ) ). % 241.74/241.86 % 241.74/241.86 cnf(cross_river_b_to_c,hypothesis, % 241.74/241.86 ( ~ cold(Situation) % 241.74/241.86 | ~ at(b,Situation) % 241.74/241.86 | at(c,skate(c,Situation)) % 241.74/241.86 | ~ situation(Situation) ) ). % 241.74/241.86 % 241.74/241.86 cnf(cross_river_c_to_b,hypothesis, % 241.74/241.86 ( ~ cold(Situation) % 241.74/241.86 | ~ at(c,Situation) % 241.74/241.86 | at(b,skate(b,Situation)) % 241.74/241.86 | ~ situation(Situation) ) ). % 241.74/241.86 % 241.74/241.86 cnf(climb_mountain_b_to_d,hypothesis, % 241.74/241.86 ( ~ warm(Situation) % 241.74/241.86 | ~ at(b,Situation) % 241.74/241.86 | at(d,climb(d,Situation)) % 241.74/241.86 | ~ situation(Situation) ) ). % 241.74/241.86 % 241.74/241.86 cnf(climb_mountain_d_to_b,hypothesis, % 241.74/241.86 ( ~ warm(Situation) % 241.74/241.86 | ~ at(d,Situation) % 241.74/241.86 | at(b,climb(b,Situation)) % 241.74/241.86 | ~ situation(Situation) ) ). % 241.74/241.86 % 241.74/241.86 cnf(go_c_to_d,hypothesis, % 241.74/241.86 ( ~ at(c,Situation) % 241.74/241.86 | at(d,go(d,Situation)) % 241.74/241.86 | ~ situation(Situation) ) ). % 241.74/241.86 % 241.74/241.86 cnf(go_d_to_c,hypothesis, % 241.74/241.86 ( ~ at(d,Situation) % 241.74/241.86 | at(c,go(c,Situation)) % 241.74/241.86 | ~ situation(Situation) ) ). % 241.74/241.86 % 241.74/241.86 cnf(go_c_to_e,hypothesis, % 241.74/241.86 ( ~ at(c,Situation) % 241.74/241.86 | at(e,go(e,Situation)) % 241.74/241.86 | ~ situation(Situation) ) ). % 241.74/241.86 % 241.74/241.86 cnf(go_e_to_c,hypothesis, % 241.74/241.86 ( ~ at(e,Situation) % 241.74/241.86 | at(c,go(c,Situation)) % 241.74/241.86 | ~ situation(Situation) ) ). % 241.74/241.86 % 241.74/241.86 cnf(go_d_to_f,hypothesis, % 241.74/241.86 ( ~ at(d,Situation) % 241.74/241.86 | at(f,go(f,Situation)) % 241.74/241.86 | ~ situation(Situation) ) ). % 241.74/241.86 % 241.74/241.86 cnf(go_f_to_d,hypothesis, % 241.74/241.86 ( ~ at(f,Situation) % 241.74/241.86 | at(d,go(d,Situation)) % 241.74/241.86 | ~ situation(Situation) ) ). % 241.74/241.86 % 241.74/241.86 cnf(initial_situation,hypothesis, % 241.74/241.86 situation(s0) ). % 241.74/241.86 % 241.74/241.86 cnf(walk_situation,hypothesis, % 241.74/241.86 ( ~ situation(Situation) % 241.74/241.86 | situation(walk(Somewhere,Situation)) ) ). % 241.74/241.86 % 241.74/241.86 cnf(drive_situation,hypothesis, % 241.74/241.86 ( ~ situation(Situation) % 241.74/241.86 | situation(drive(Somewhere,Situation)) ) ). % 241.74/241.86 % 241.74/241.86 cnf(climb_situation,hypothesis, % 241.74/241.86 ( ~ situation(Situation) % 241.74/241.86 | situation(climb(Somewhere,Situation)) ) ). % 241.74/241.86 % 241.74/241.86 cnf(skate_situation,hypothesis, % 241.74/241.86 ( ~ situation(Situation) % 241.74/241.86 | situation(skate(Somewhere,Situation)) ) ). % 241.74/241.86 % 241.74/241.86 cnf(go_situation,hypothesis, % 241.74/241.86 ( ~ situation(Situation) % 241.74/241.86 | situation(go(Somewhere,Situation)) ) ). % 241.74/241.86 % 241.74/241.86 cnf(initial,hypothesis, % 241.74/241.86 at(f,s0) ). % 241.74/241.86 % 241.74/241.86 cnf(prove_you_can_get_to_a_in_a_situation,negated_conjecture, % 241.74/241.86 ( ~ at(a,S) % 241.74/241.86 | ~ situation(S) ) ). % 241.74/241.86 % 241.74/241.86 %-------------------------------------------------------------------------- % 241.74/241.86 %------------------------------------------- % 241.74/241.86 % Proof found % 241.74/241.86 % SZS status Theorem for theBenchmark % 241.74/241.86 % SZS output start Proof % 241.81/241.92 %ClaNum:23(EqnAxiom:0) % 241.81/241.92 %VarNum:61(SingletonVarNum:25) % 241.81/241.92 %MaxLitNum:4 % 241.81/241.92 %MaxfuncDepth:1 % 241.81/241.92 %SharedTerms:9 % 241.81/241.92 %goalClause: 4 % 241.81/241.92 [1]P1(a1) % 241.81/241.92 [2]P2(a2,a1) % 241.81/241.92 [4]~P1(x41)+~P2(a3,x41) % 241.81/241.92 [5]~P1(x52)+P1(f11(x51,x52)) % 241.81/241.92 [6]~P1(x62)+P1(f4(x61,x62)) % 241.81/241.92 [7]~P1(x72)+P1(f12(x71,x72)) % 241.81/241.92 [8]~P1(x82)+P1(f5(x81,x82)) % 241.81/241.92 [9]~P1(x92)+P1(f10(x91,x92)) % 241.81/241.92 [10]~P1(x101)+~P2(a6,x101)+P2(a3,f11(a3,x101)) % 241.81/241.92 [11]~P1(x111)+~P2(a6,x111)+P2(a3,f4(a3,x111)) % 241.81/241.92 [14]~P1(x141)+~P2(a8,x141)+P2(a7,f10(a7,x141)) % 241.81/241.92 [15]~P1(x151)+~P2(a9,x151)+P2(a7,f10(a7,x151)) % 241.81/241.92 [16]~P1(x161)+~P2(a7,x161)+P2(a8,f10(a8,x161)) % 241.81/241.92 [17]~P1(x171)+~P2(a2,x171)+P2(a8,f10(a8,x171)) % 241.81/241.92 [18]~P1(x181)+~P2(a7,x181)+P2(a9,f10(a9,x181)) % 241.81/241.92 [19]~P1(x191)+~P2(a8,x191)+P2(a2,f10(a2,x191)) % 241.81/241.92 [20]~P3(x201)+~P1(x201)+~P2(a7,x201)+P2(a6,f12(a6,x201)) % 241.81/241.92 [21]~P4(x211)+~P1(x211)+~P2(a8,x211)+P2(a6,f5(a6,x211)) % 241.81/241.92 [22]~P3(x221)+~P1(x221)+~P2(a6,x221)+P2(a7,f12(a7,x221)) % 241.81/241.92 [23]~P4(x231)+~P1(x231)+~P2(a6,x231)+P2(a8,f5(a8,x231)) % 241.81/241.92 [3]~P1(x32)+~P1(x31)+P4(x31)+P3(x32) % 241.81/241.92 %EqnAxiom % 241.81/241.92 % 241.81/241.92 %------------------------------------------- % 242.52/242.62 cnf(24,plain, % 242.52/242.62 (~P2(a3,f11(x241,a1))), % 242.52/242.62 inference(scs_inference,[],[1,4,5])). % 242.52/242.62 cnf(28,plain, % 242.52/242.62 (P1(f4(x281,f12(x282,a1)))), % 242.52/242.62 inference(scs_inference,[],[1,6,7])). % 242.52/242.62 cnf(32,plain, % 242.52/242.62 (P1(f5(x321,f10(x322,a1)))), % 242.52/242.62 inference(scs_inference,[],[1,8,9])). % 242.52/242.62 cnf(1561,plain, % 242.52/242.62 (~P2(a3,f4(x15611,f4(x15612,f12(x15613,a1))))), % 242.52/242.62 inference(scs_inference,[],[28,4,6])). % 242.52/242.62 cnf(2331,plain, % 242.52/242.62 (~P2(a3,f11(x23311,f5(x23312,f10(x23313,a1))))), % 242.52/242.62 inference(scs_inference,[],[32,4,5])). % 242.52/242.62 cnf(593987,plain, % 242.52/242.62 (P1(f11(x5939871,a1))), % 242.52/242.62 inference(scs_inference,[],[1,4,5])). % 242.52/242.62 cnf(593993,plain, % 242.52/242.62 (P1(f5(x5939931,a1))), % 242.52/242.62 inference(scs_inference,[],[1,4,5,6,7,8])). % 242.52/242.62 cnf(593995,plain, % 242.52/242.62 (P1(f10(x5939951,a1))), % 242.52/242.62 inference(scs_inference,[],[1,4,5,6,7,8,9])). % 242.52/242.62 cnf(593997,plain, % 242.52/242.62 (P2(a8,f10(a8,a1))), % 242.52/242.62 inference(scs_inference,[],[1,2,4,5,6,7,8,9,17])). % 242.52/242.62 cnf(1052833,plain, % 242.52/242.62 (~P4(f10(a8,a1))), % 242.52/242.62 inference(scs_inference,[],[2331,32,593997,593995,4,10,21])). % 242.52/242.62 cnf(1054429,plain, % 242.52/242.62 (~P2(a3,f4(x10544291,f11(x10544292,a1)))), % 242.52/242.62 inference(scs_inference,[],[593987,4,6])). % 242.52/242.62 cnf(1056105,plain, % 242.52/242.62 (P1(f11(x10561051,f5(x10561052,a1)))), % 242.52/242.62 inference(scs_inference,[],[593993,8,7,5])). % 242.52/242.62 cnf(1056107,plain, % 242.52/242.62 (P1(f10(x10561071,f5(x10561072,a1)))), % 242.52/242.62 inference(scs_inference,[],[593993,8,7,5,9])). % 242.52/242.62 cnf(1056115,plain, % 242.52/242.62 (P1(f10(x10561151,a1))), % 242.52/242.62 inference(rename_variables,[],[593995])). % 242.52/242.62 cnf(1056120,plain, % 242.52/242.62 (P2(a7,f10(a7,f10(a8,a1)))), % 242.52/242.62 inference(scs_inference,[],[1,24,593993,593995,1056115,593987,593997,1054429,8,7,5,9,6,10,19,11,14])). % 242.52/242.62 cnf(1056141,plain, % 242.52/242.62 (P1(f10(x10561411,f10(x10561412,a1)))), % 242.52/242.62 inference(scs_inference,[],[593995,32,8,7,5,9])). % 242.52/242.62 cnf(1056151,plain, % 242.52/242.62 (P2(a8,f10(a8,f10(a7,f10(a8,a1))))), % 242.52/242.62 inference(scs_inference,[],[1,24,593995,32,593987,1054429,1056120,8,7,5,9,6,10,11,16])). % 242.52/242.62 cnf(1056153,plain, % 242.52/242.62 (P2(a9,f10(a9,f10(a7,f10(a8,a1))))), % 242.52/242.62 inference(scs_inference,[],[1,24,593995,32,593987,1054429,1056120,8,7,5,9,6,10,11,16,18])). % 242.52/242.62 cnf(1056315,plain, % 242.52/242.62 (P1(f11(x10563151,f10(x10563152,f5(x10563153,a1))))), % 242.52/242.62 inference(scs_inference,[],[1,1056107,1056105,4,8,5])). % 242.52/242.62 cnf(1056317,plain, % 242.52/242.62 (P1(f4(x10563171,f11(x10563172,f5(x10563173,a1))))), % 242.52/242.62 inference(scs_inference,[],[1,1056107,1056105,4,8,5,6])). % 242.52/242.62 cnf(1057359,plain, % 242.52/242.62 (P1(f4(x10573591,f4(x10573592,f11(x10573593,f5(x10573594,a1)))))), % 242.52/242.62 inference(scs_inference,[],[1,1056315,1056317,4,8,9,6])). % 242.52/242.62 cnf(1057361,plain, % 242.52/242.62 (P1(f11(x10573611,f11(x10573612,f10(x10573613,f5(x10573614,a1)))))), % 242.52/242.62 inference(scs_inference,[],[1,1056315,1056317,4,8,9,6,5])). % 242.52/242.62 cnf(1220943,plain, % 242.52/242.62 (P1(f4(x12209431,f10(x12209432,f10(x12209433,a1))))), % 242.52/242.62 inference(scs_inference,[],[1057359,1056141,5,6])). % 242.52/242.62 cnf(1220947,plain, % 242.52/242.62 (P1(f5(x12209471,f10(x12209472,f10(x12209473,a1))))), % 242.52/242.62 inference(scs_inference,[],[1057359,1056141,5,6,7,8])). % 242.52/242.62 cnf(1256307,plain, % 242.52/242.62 (P1(f11(x12563071,f10(x12563072,f10(x12563073,a1))))), % 242.52/242.62 inference(scs_inference,[],[1056141,5])). % 242.52/242.62 cnf(1256311,plain, % 242.52/242.62 (P1(f12(x12563111,f10(x12563112,f10(x12563113,a1))))), % 242.52/242.62 inference(scs_inference,[],[1056141,1220943,5,8,7])). % 242.52/242.62 cnf(1256315,plain, % 242.52/242.62 (P1(f10(x12563151,f10(x12563152,f10(x12563153,a1))))), % 242.52/242.62 inference(scs_inference,[],[1056141,1220943,5,8,7,6,9])). % 242.52/242.62 cnf(1256326,plain, % 242.52/242.62 (P2(a7,f10(a7,f10(a8,f10(a7,f10(a8,a1)))))), % 242.52/242.62 inference(scs_inference,[],[24,1,28,1056141,1056151,1561,1220943,5,8,7,6,9,4,10,11,14])). % 242.52/242.62 cnf(1256362,plain, % 242.52/242.62 (P2(a7,f10(a7,f10(a9,f10(a7,f10(a8,a1)))))), % 242.52/242.62 inference(scs_inference,[],[24,1,28,1220943,1561,1056153,1220947,1256315,8,7,5,6,9,4,10,11,15])). % 242.52/242.62 cnf(1256418,plain, % 242.52/242.62 (P1(f10(x12564181,f10(x12564182,f10(x12564183,f10(x12564184,a1)))))), % 242.52/242.62 inference(scs_inference,[],[1256315,1256307,5,8,6,7,9])). % 242.52/242.62 cnf(1256424,plain, % 242.52/242.62 (P2(a9,f10(a9,f10(a7,f10(a9,f10(a7,f10(a8,a1))))))), % 242.52/242.62 inference(scs_inference,[],[1,1256315,1256362,1256307,5,8,6,7,9,4,16,18])). % 242.52/242.62 cnf(1256452,plain, % 242.52/242.62 (P1(f4(x12564521,f12(x12564522,f10(x12564523,f10(x12564524,a1)))))), % 242.52/242.62 inference(scs_inference,[],[1256307,1256311,5,8,7,6])). % 242.52/242.62 cnf(1256501,plain, % 242.52/242.62 (P3(f10(x12565011,f10(x12565012,a1)))), % 242.52/242.62 inference(scs_inference,[],[1,1052833,1056141,593995,4,3])). % 242.52/242.62 cnf(1257120,plain, % 242.52/242.62 (P2(a3,f4(a3,f12(a6,f10(a7,f10(a8,a1)))))), % 242.52/242.62 inference(scs_inference,[],[1256501,1057361,1256326,1256424,1256418,1256311,1056120,1056141,1052833,593995,16,20,3,15,11])). % 242.52/242.62 cnf(1257140,plain, % 242.52/242.62 ($false), % 242.52/242.62 inference(scs_inference,[],[1257120,1256452,4]), % 242.52/242.62 ['proof']). % 243.15/243.21 % SZS output end Proof % 243.15/243.21 % Total time :241.080000s %------------------------------------------------------------------------------