%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ008-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 : n029.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:42:01 EDT 2024 % Result : Unsatisfiable 0.53s 0.60s % Output : CNFRefutation 0.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : PUZ008-1 : TPTP v8.2.0. Released v1.0.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n029.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Jun 18 10:49:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 0.53/0.59 %------------------------------------------- % 0.53/0.59 % File :CSE---1.7 % 0.53/0.59 % Problem :theBenchmark % 0.53/0.59 % Transform :cnf % 0.53/0.59 % Format :tptp:raw % 0.53/0.59 % Command :java -jar mcs_scs.jar %d %s % 0.53/0.59 % 0.53/0.59 % Result :Theorem 0.000000s % 0.53/0.59 % Output :CNFRefutation 0.000000s % 0.53/0.59 %------------------------------------------- % 0.53/0.60 %-------------------------------------------------------------------------- % 0.53/0.60 % File : PUZ008-1 : TPTP v8.2.0. Released v1.0.0. % 0.53/0.60 % Domain : Puzzles % 0.53/0.60 % Problem : Missionaries and Cannibals % 0.53/0.60 % Version : Especial. % 0.53/0.60 % Theorem formulation : Declarative. % 0.53/0.60 % English : There are 3 missionaries, 3 cannibals, and a boat on the west % 0.53/0.60 % bank of a river. All wish to cross, but the boat holds % 0.53/0.60 % at most 2 people. If the cannibals ever outnumber the % 0.53/0.60 % missionaries on either bank of the river the outnumbered % 0.53/0.60 % missionaries will be eaten. Can they all safely cross the % 0.53/0.60 % river? If so, how? (The boat cannot cross empty.) % 0.53/0.60 % 0.53/0.60 % Refs : [WO+92] Wos et al. (1992), Automated Reasoning: Introduction a % 0.53/0.60 % : [Rap95] Raptis (1995), Email to G. Sutcliffe % 0.53/0.60 % Source : [ANL] % 0.53/0.60 % Names : mission.ver1.in [ANL] % 0.53/0.60 % 0.53/0.60 % Status : Unsatisfiable % 0.53/0.60 % Rating : 0.00 v5.3.0, 0.05 v5.2.0, 0.00 v3.7.0, 0.14 v3.4.0, 0.20 v3.3.0, 0.00 v2.0.0 % 0.53/0.60 % Syntax : Number of clauses : 16 ( 6 unt; 0 nHn; 12 RR) % 0.53/0.60 % Number of literals : 26 ( 0 equ; 11 neg) % 0.53/0.60 % Maximal clause size : 2 ( 1 avg) % 0.53/0.60 % Maximal term depth : 6 ( 2 avg) % 0.53/0.60 % Number of predicates : 1 ( 1 usr; 0 prp; 3-3 aty) % 0.53/0.60 % Number of functors : 8 ( 8 usr; 3 con; 0-2 aty) % 0.53/0.60 % Number of variables : 57 ( 13 sgn) % 0.53/0.60 % SPC : CNF_UNS_RFO_NEQ_HRN % 0.53/0.60 % 0.53/0.60 % Comments : Dimitris Raptis has pointed out [Rap95] that this formulation % 0.53/0.60 % allows a trivial solution to be found. This is due to 4 clauses % 0.53/0.60 % that [WO+92] add in for forward subsumption purposes only (I % 0.53/0.60 % don't know of any ATP system that has a "for subsumption only" % 0.53/0.60 % subset of the input clauses - might be worth researching). If % 0.53/0.60 % those clauses are omitted, an illegal solution can be found. % 0.53/0.60 %-------------------------------------------------------------------------- % 0.53/0.60 %----Moving cannibals only % 0.53/0.60 cnf(cannibal_west_to_east,axiom, % 0.53/0.60 ( ~ achievable(west(m(X),c(s(Y))),boatonwest,east(m(Z),c(W))) % 0.53/0.60 | achievable(west(m(X),c(Y)),boatoneast,east(m(Z),c(s(W)))) ) ). % 0.53/0.60 % 0.53/0.60 cnf(cannibal_east_to_west,axiom, % 0.53/0.60 ( ~ achievable(west(m(X),c(Y)),boatoneast,east(m(Z),c(s(W)))) % 0.53/0.60 | achievable(west(m(X),c(s(Y))),boatonwest,east(m(Z),c(W))) ) ). % 0.53/0.60 % 0.53/0.60 cnf(two_cannibals_west_to_east,axiom, % 0.53/0.60 ( ~ achievable(west(m(X),c(s(s(Y)))),boatonwest,east(m(Z),c(W))) % 0.53/0.60 | achievable(west(m(X),c(Y)),boatoneast,east(m(Z),c(s(s(W))))) ) ). % 0.53/0.60 % 0.53/0.60 cnf(two_cannibals_east_to_west,axiom, % 0.53/0.60 ( ~ achievable(west(m(X),c(Y)),boatoneast,east(m(Z),c(s(s(W))))) % 0.53/0.60 | achievable(west(m(X),c(s(s(Y)))),boatonwest,east(m(Z),c(W))) ) ). % 0.53/0.60 % 0.53/0.60 %----Moving missionaries only % 0.53/0.60 cnf(missionary_west_to_east,axiom, % 0.53/0.60 ( ~ achievable(west(m(s(X)),c(Y)),boatonwest,east(m(Z),c(W))) % 0.53/0.60 | achievable(west(m(X),c(Y)),boatoneast,east(m(s(Z)),c(W))) ) ). % 0.53/0.60 % 0.53/0.60 cnf(missionary_east_to_west,axiom, % 0.53/0.60 ( ~ achievable(west(m(X),c(Y)),boatoneast,east(m(s(Z)),c(W))) % 0.53/0.60 | achievable(west(m(s(X)),c(Y)),boatonwest,east(m(Z),c(W))) ) ). % 0.53/0.60 % 0.53/0.60 cnf(two_missionaries_west_to_east,axiom, % 0.53/0.60 ( ~ achievable(west(m(s(s(X))),c(Y)),boatonwest,east(m(Z),c(W))) % 0.53/0.60 | achievable(west(m(X),c(Y)),boatoneast,east(m(s(s(Z))),c(W))) ) ). % 0.53/0.60 % 0.53/0.60 cnf(two_missionaries_east_to_west,axiom, % 0.53/0.60 ( ~ achievable(west(m(X),c(Y)),boatoneast,east(m(s(s(Z))),c(W))) % 0.53/0.60 | achievable(west(m(s(s(X))),c(Y)),boatonwest,east(m(Z),c(W))) ) ). % 0.53/0.60 % 0.53/0.60 %----Moving a missionary and a cannibal % 0.53/0.60 cnf(missionary_and_cannibal_west_to_east,axiom, % 0.53/0.60 ( ~ achievable(west(m(s(X)),c(s(Y))),boatonwest,east(m(Z),c(W))) % 0.53/0.60 | achievable(west(m(X),c(Y)),boatoneast,east(m(s(Z)),c(s(W)))) ) ). % 0.53/0.60 % 0.53/0.60 cnf(missionary_and_cannibal_east_to_west,axiom, % 0.53/0.60 ( ~ achievable(west(m(X),c(Y)),boatoneast,east(m(s(Z)),c(s(W)))) % 0.53/0.60 | achievable(west(m(s(X)),c(s(Y))),boatonwest,east(m(Z),c(W))) ) ). % 0.53/0.60 % 0.53/0.60 %----The next four clauses should only be used for forward subsumption. % 0.53/0.60 %----In OTTER they would be put in the passive list. For other ATP % 0.53/0.60 %----systems, these clauses allow a trivial solution to be found. But % 0.53/0.60 %----if they are omitted, an illegal solution can be found. % 0.53/0.60 cnf(extra_cannibal_meal_on_west_bank,axiom, % 0.53/0.60 achievable(west(m(s(X)),c(s(s(X)))),Y,east(Z,W)) ). % 0.53/0.60 % 0.53/0.60 cnf(two_extra_cannibals_meal_on_west_bank,axiom, % 0.53/0.60 achievable(west(m(s(X)),c(s(s(s(X))))),Y,east(Z,W)) ). % 0.53/0.60 % 0.53/0.60 cnf(extra_cannibal_meal_on_east_bank,axiom, % 0.53/0.60 achievable(west(X,Y),Z,east(m(s(W)),c(s(s(W))))) ). % 0.53/0.60 % 0.53/0.60 cnf(two_extra_cannibals_meal_on_east_bank,axiom, % 0.53/0.60 achievable(west(X,Y),Z,east(m(s(W)),c(s(s(s(W)))))) ). % 0.53/0.60 % 0.53/0.60 cnf(start_on_west_bank,hypothesis, % 0.53/0.60 achievable(west(m(s(s(s(n0)))),c(s(s(s(n0))))),boatonwest,east(m(n0),c(n0))) ). % 0.53/0.60 % 0.53/0.60 cnf(prove_can_get_to_east_bank,negated_conjecture, % 0.53/0.60 ~ achievable(west(m(n0),c(n0)),X,east(m(s(s(s(n0)))),c(s(s(s(n0)))))) ). % 0.53/0.60 % 0.53/0.60 %-------------------------------------------------------------------------- % 0.53/0.60 %------------------------------------------- % 0.53/0.60 % Proof found % 0.53/0.60 % SZS status Theorem for theBenchmark % 0.53/0.60 % SZS output start Proof % 0.55/0.60 %ClaNum:16(EqnAxiom:0) % 0.55/0.60 %VarNum:101(SingletonVarNum:57) % 0.55/0.60 %MaxLitNum:2 % 0.55/0.60 %MaxfuncDepth:5 % 0.55/0.60 %SharedTerms:15 % 0.55/0.60 %goalClause: 6 % 0.55/0.60 %singleGoalClaCount:1 % 0.55/0.60 [5]P1(f1(f3(f2(f2(f2(a8)))),f4(f2(f2(f2(a8))))),a5,f7(f3(a8),f4(a8))) % 0.55/0.60 [6]~P1(f1(f3(a8),f4(a8)),x61,f7(f3(f2(f2(f2(a8)))),f4(f2(f2(f2(a8)))))) % 0.55/0.60 [1]P1(f1(x11,x12),x13,f7(f3(f2(x14)),f4(f2(f2(x14))))) % 0.55/0.60 [2]P1(f1(f3(f2(x21)),f4(f2(f2(x21)))),x22,f7(x23,x24)) % 0.55/0.60 [3]P1(f1(x31,x32),x33,f7(f3(f2(x34)),f4(f2(f2(f2(x34)))))) % 0.55/0.60 [4]P1(f1(f3(f2(x41)),f4(f2(f2(f2(x41))))),x42,f7(x43,x44)) % 0.55/0.60 [8]P1(f1(f3(x81),f4(x82)),a6,f7(f3(f2(x83)),f4(x84)))+~P1(f1(f3(f2(x81)),f4(x82)),a5,f7(f3(x83),f4(x84))) % 0.55/0.60 [10]P1(f1(f3(f2(x101)),f4(x102)),a5,f7(f3(x103),f4(x104)))+~P1(f1(f3(x101),f4(x102)),a6,f7(f3(f2(x103)),f4(x104))) % 0.55/0.60 [14]P1(f1(f3(x141),f4(x142)),a6,f7(f3(f2(f2(x143))),f4(x144)))+~P1(f1(f3(f2(f2(x141))),f4(x142)),a5,f7(f3(x143),f4(x144))) % 0.55/0.60 [16]P1(f1(f3(f2(f2(x161))),f4(x162)),a5,f7(f3(x163),f4(x164)))+~P1(f1(f3(x161),f4(x162)),a6,f7(f3(f2(f2(x163))),f4(x164))) % 0.55/0.60 [7]~P1(f1(f3(x71),f4(f2(x72))),a5,f7(f3(x73),f4(x74)))+P1(f1(f3(x71),f4(x72)),a6,f7(f3(x73),f4(f2(x74)))) % 0.55/0.60 [9]~P1(f1(f3(x91),f4(x92)),a6,f7(f3(x93),f4(f2(x94))))+P1(f1(f3(x91),f4(f2(x92))),a5,f7(f3(x93),f4(x94))) % 0.55/0.60 [11]~P1(f1(f3(f2(x111)),f4(f2(x112))),a5,f7(f3(x113),f4(x114)))+P1(f1(f3(x111),f4(x112)),a6,f7(f3(f2(x113)),f4(f2(x114)))) % 0.55/0.60 [12]~P1(f1(f3(x121),f4(x122)),a6,f7(f3(f2(x123)),f4(f2(x124))))+P1(f1(f3(f2(x121)),f4(f2(x122))),a5,f7(f3(x123),f4(x124))) % 0.55/0.60 [13]~P1(f1(f3(x131),f4(f2(f2(x132)))),a5,f7(f3(x133),f4(x134)))+P1(f1(f3(x131),f4(x132)),a6,f7(f3(x133),f4(f2(f2(x134))))) % 0.55/0.60 [15]~P1(f1(f3(x151),f4(x152)),a6,f7(f3(x153),f4(f2(f2(x154)))))+P1(f1(f3(x151),f4(f2(f2(x152)))),a5,f7(f3(x153),f4(x154))) % 0.55/0.60 %EqnAxiom % 0.55/0.60 % 0.55/0.60 %------------------------------------------- % 0.55/0.60 cnf(17,plain, % 0.55/0.60 ($false), % 0.55/0.60 inference(scs_inference,[],[6,1,8]), % 0.55/0.60 ['proof']). % 0.55/0.60 % SZS output end Proof % 0.55/0.60 % Total time :0.000000s %------------------------------------------------------------------------------