%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ022-1 : TPTP v8.2.0. Released v1.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n024.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:05 EDT 2024 % Result : Unsatisfiable 0.55s 0.68s % Output : CNFRefutation 0.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.07 % Problem : PUZ022-1 : TPTP v8.2.0. Released v1.1.0. % 0.02/0.07 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.06/0.26 % Computer : n024.cluster.edu % 0.06/0.26 % Model : x86_64 x86_64 % 0.06/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.26 % Memory : 8042.1875MB % 0.06/0.26 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.26 % CPULimit : 300 % 0.06/0.26 % WCLimit : 300 % 0.06/0.26 % DateTime : Tue Jun 18 10:55:53 EDT 2024 % 0.06/0.26 % CPUTime : % 0.11/0.45 start to proof:theBenchmark % 0.55/0.67 %------------------------------------------- % 0.55/0.67 % File :CSE---1.7 % 0.55/0.67 % Problem :theBenchmark % 0.55/0.67 % Transform :cnf % 0.55/0.67 % Format :tptp:raw % 0.55/0.67 % Command :java -jar mcs_scs.jar %d %s % 0.55/0.67 % 0.55/0.67 % Result :Theorem 0.190000s % 0.55/0.67 % Output :CNFRefutation 0.190000s % 0.55/0.67 %------------------------------------------- % 0.55/0.67 %-------------------------------------------------------------------------- % 0.55/0.67 % File : PUZ022-1 : TPTP v8.2.0. Released v1.1.0. % 0.55/0.67 % Domain : Puzzles % 0.55/0.67 % Problem : An ocean that borders on two adjacent Australian states % 0.55/0.67 % Version : Especial. % 0.55/0.67 % English : There is a database of assertions about Australian states and % 0.55/0.67 % oceans and their relationships. Find which ocean borders % 0.55/0.67 % on two adjacent Australian states. % 0.55/0.67 % 0.55/0.67 % Refs : [Pla82] Plaisted (1982), A Simplified Problem Reduction Format % 0.55/0.67 % Source : [TPTP] % 0.55/0.67 % Names : % 0.55/0.67 % 0.55/0.67 % Status : Unsatisfiable % 0.55/0.67 % Rating : 0.00 v2.0.0 % 0.55/0.67 % Syntax : Number of clauses : 33 ( 31 unt; 0 nHn; 33 RR) % 0.55/0.67 % Number of literals : 39 ( 0 equ; 7 neg) % 0.55/0.67 % Maximal clause size : 6 ( 1 avg) % 0.55/0.67 % Maximal term depth : 1 ( 1 avg) % 0.55/0.67 % Number of predicates : 3 ( 3 usr; 0 prp; 1-2 aty) % 0.55/0.67 % Number of functors : 11 ( 11 usr; 11 con; 0-0 aty) % 0.55/0.67 % Number of variables : 5 ( 0 sgn) % 0.55/0.67 % SPC : CNF_UNS_EPR_NEQ_HRN % 0.55/0.67 % 0.55/0.67 % Comments : Inspired by Problem 5.6 in [Pla82] % 0.55/0.67 %-------------------------------------------------------------------------- % 0.55/0.67 cnf(symmetry_of_borders,axiom, % 0.55/0.67 ( ~ borders(Y,X) % 0.55/0.67 | borders(X,Y) ) ). % 0.55/0.67 % 0.55/0.67 cnf(atlantic,negated_conjecture, % 0.55/0.67 ocean(atlantic) ). % 0.55/0.67 % 0.55/0.67 cnf(indian,negated_conjecture, % 0.55/0.67 ocean(indian) ). % 0.55/0.67 % 0.55/0.67 cnf(pacific,negated_conjecture, % 0.55/0.67 ocean(pacific) ). % 0.55/0.67 % 0.55/0.67 cnf(southern,negated_conjecture, % 0.55/0.67 ocean(southern) ). % 0.55/0.67 % 0.55/0.67 cnf(western_australia,negated_conjecture, % 0.55/0.67 state(western_australia) ). % 0.55/0.67 % 0.55/0.67 cnf(northern_territory,negated_conjecture, % 0.55/0.67 state(northern_territory) ). % 0.55/0.67 % 0.55/0.67 cnf(queensland,negated_conjecture, % 0.55/0.67 state(queensland) ). % 0.55/0.67 % 0.55/0.67 cnf(south_australia,negated_conjecture, % 0.55/0.67 state(south_australia) ). % 0.55/0.67 % 0.55/0.67 cnf(new_south_wales,negated_conjecture, % 0.55/0.67 state(new_south_wales) ). % 0.55/0.67 % 0.55/0.67 cnf(victoria,negated_conjecture, % 0.55/0.67 state(victoria) ). % 0.55/0.67 % 0.55/0.67 cnf(tasmania,negated_conjecture, % 0.55/0.67 state(tasmania) ). % 0.55/0.67 % 0.55/0.67 cnf(wa_nt,negated_conjecture, % 0.55/0.67 borders(western_australia,northern_territory) ). % 0.55/0.67 % 0.55/0.67 cnf(wa_sa,negated_conjecture, % 0.55/0.67 borders(western_australia,south_australia) ). % 0.55/0.67 % 0.55/0.67 cnf(sa_nt,negated_conjecture, % 0.55/0.67 borders(south_australia,northern_territory) ). % 0.55/0.67 % 0.55/0.67 cnf(sa_qld,negated_conjecture, % 0.55/0.67 borders(south_australia,queensland) ). % 0.55/0.67 % 0.55/0.67 cnf(sa_nsw,negated_conjecture, % 0.55/0.67 borders(south_australia,new_south_wales) ). % 0.55/0.67 % 0.55/0.67 cnf(sa_vic,negated_conjecture, % 0.55/0.67 borders(south_australia,victoria) ). % 0.55/0.67 % 0.55/0.67 cnf(nt_qld,negated_conjecture, % 0.55/0.68 borders(northern_territory,queensland) ). % 0.55/0.68 % 0.55/0.68 cnf(qld_nsw,negated_conjecture, % 0.55/0.68 borders(queensland,new_south_wales) ). % 0.55/0.68 % 0.55/0.68 cnf(nsw_vic,negated_conjecture, % 0.55/0.68 borders(new_south_wales,victoria) ). % 0.55/0.68 % 0.55/0.68 cnf(indian_wa,negated_conjecture, % 0.55/0.68 borders(indian,western_australia) ). % 0.55/0.68 % 0.55/0.68 cnf(indian_nt,negated_conjecture, % 0.55/0.68 borders(indian,northern_territory) ). % 0.55/0.68 % 0.55/0.68 cnf(indian_qld,negated_conjecture, % 0.55/0.68 borders(indian,queensland) ). % 0.55/0.68 % 0.55/0.68 cnf(southern_wa,negated_conjecture, % 0.55/0.68 borders(southern,western_australia) ). % 0.55/0.68 % 0.55/0.68 cnf(southern_sa,negated_conjecture, % 0.55/0.68 borders(southern,south_australia) ). % 0.55/0.68 % 0.55/0.68 cnf(southern_vic,negated_conjecture, % 0.55/0.68 borders(southern,victoria) ). % 0.55/0.68 % 0.55/0.68 cnf(southern_tas,negated_conjecture, % 0.55/0.68 borders(southern,tasmania) ). % 0.55/0.68 % 0.55/0.68 cnf(pacific_qld,negated_conjecture, % 0.55/0.68 borders(pacific,queensland) ). % 0.55/0.68 % 0.55/0.68 cnf(pacific_nsw,negated_conjecture, % 0.55/0.68 borders(pacific,new_south_wales) ). % 0.55/0.68 % 0.55/0.68 cnf(pacific_vic,negated_conjecture, % 0.55/0.68 borders(pacific,victoria) ). % 0.55/0.68 % 0.55/0.68 cnf(pacific_tas,negated_conjecture, % 0.55/0.68 borders(pacific,tasmania) ). % 0.55/0.68 % 0.55/0.68 cnf(prove_borders,negated_conjecture, % 0.55/0.68 ( ~ state(State1) % 0.55/0.68 | ~ state(State2) % 0.55/0.68 | ~ borders(State1,State2) % 0.55/0.68 | ~ borders(State1,Ocean) % 0.55/0.68 | ~ borders(State2,Ocean) % 0.55/0.68 | ~ ocean(Ocean) ) ). % 0.55/0.68 % 0.55/0.68 %-------------------------------------------------------------------------- % 0.55/0.68 %------------------------------------------- % 0.55/0.68 % Proof found % 0.55/0.68 % SZS status Theorem for theBenchmark % 0.55/0.68 % SZS output start Proof % 0.55/0.68 %ClaNum:33(EqnAxiom:0) % 0.55/0.68 %VarNum:13(SingletonVarNum:5) % 0.55/0.68 %MaxLitNum:6 % 0.55/0.68 %MaxfuncDepth:0 % 0.55/0.68 %SharedTerms:42 % 0.55/0.68 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 33 % 0.55/0.68 %singleGoalClaCount:31 % 0.55/0.68 [1]P1(a1) % 0.55/0.68 [2]P1(a2) % 0.55/0.68 [3]P1(a3) % 0.55/0.68 [4]P1(a6) % 0.55/0.68 [5]P3(a9) % 0.55/0.68 [6]P3(a4) % 0.55/0.68 [7]P3(a7) % 0.55/0.68 [8]P3(a8) % 0.55/0.68 [9]P3(a5) % 0.55/0.68 [10]P3(a10) % 0.55/0.68 [11]P3(a11) % 0.55/0.68 [12]P2(a2,a9) % 0.55/0.68 [13]P2(a2,a4) % 0.55/0.68 [14]P2(a2,a7) % 0.55/0.68 [15]P2(a3,a7) % 0.55/0.68 [16]P2(a3,a5) % 0.55/0.68 [17]P2(a3,a10) % 0.55/0.68 [18]P2(a3,a11) % 0.55/0.68 [19]P2(a6,a9) % 0.55/0.68 [20]P2(a6,a8) % 0.55/0.68 [21]P2(a6,a10) % 0.55/0.68 [22]P2(a6,a11) % 0.55/0.68 [23]P2(a9,a4) % 0.55/0.68 [24]P2(a9,a8) % 0.55/0.68 [25]P2(a4,a7) % 0.55/0.68 [26]P2(a7,a5) % 0.55/0.68 [27]P2(a8,a4) % 0.55/0.68 [28]P2(a8,a7) % 0.55/0.68 [29]P2(a8,a5) % 0.55/0.68 [30]P2(a8,a10) % 0.55/0.68 [31]P2(a5,a10) % 0.55/0.68 [32]~P2(x322,x321)+P2(x321,x322) % 0.55/0.68 [33]~P2(x332,x331)+~P2(x333,x331)+~P2(x333,x332)+~P1(x331)+~P3(x332)+~P3(x333) % 0.55/0.68 %EqnAxiom % 0.55/0.68 % 0.55/0.68 %------------------------------------------- % 0.55/0.68 cnf(182,plain, % 0.55/0.68 (~P2(a9,a2)), % 0.55/0.68 inference(scs_inference,[],[2,13,5,6,23,33,32])). % 0.55/0.68 cnf(183,plain, % 0.55/0.68 ($false), % 0.55/0.68 inference(scs_inference,[],[12,182,32]), % 0.55/0.68 ['proof']). % 0.55/0.68 % SZS output end Proof % 0.55/0.68 % Total time :0.190000s %------------------------------------------------------------------------------