%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ001+2 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n025.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:00 EDT 2024 % Result : Theorem 0.55s 0.85s % Output : CNFRefutation 0.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : PUZ001+2 : TPTP v8.2.0. Released v4.0.0. % 0.10/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n025.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Tue Jun 18 10:33:39 EDT 2024 % 0.13/0.33 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 0.55/0.84 %------------------------------------------- % 0.55/0.84 % File :CSE---1.7 % 0.55/0.84 % Problem :theBenchmark % 0.55/0.84 % Transform :cnf % 0.55/0.84 % Format :tptp:raw % 0.55/0.84 % Command :java -jar mcs_scs.jar %d %s % 0.55/0.84 % 0.55/0.84 % Result :Theorem 0.240000s % 0.55/0.84 % Output :CNFRefutation 0.240000s % 0.55/0.84 %------------------------------------------- % 0.55/0.85 %------------------------------------------------------------------------------ % 0.55/0.85 % File : PUZ001+2 : TPTP v8.2.0. Released v4.0.0. % 0.55/0.85 % Domain : Puzzles % 0.55/0.85 % Problem : Dreadbury Mansion % 0.55/0.85 % Version : Especial. % 0.55/0.85 % Theorem formulation : Converted from ACE by the APE [FKK08]. % 0.55/0.85 % English : Someone who lives in DreadburyMansion kills AuntAgatha. If % 0.55/0.85 % somebody X lives in DreadburyMansion then X is AuntAgatha or X % 0.55/0.85 % is the Butler or X is Charles. Everyone hates everyone that he % 0.55/0.85 % kills. Noone is richer than someone that he kills. Charles hates % 0.55/0.85 % noone who is hated by AuntAgatha. AuntAgatha does not hate the % 0.55/0.85 % Butler. Everyone that is not the Butler is hated by AuntAgatha. % 0.55/0.85 % The Butler hates everyone who is not richer than AuntAgatha. The % 0.55/0.85 % Butler hates everyone who is hated by AuntAgatha. Noone hates % 0.55/0.85 % everyone. AuntAgatha is not the Butler. Therefore, AuntAgatha % 0.55/0.85 % kills AuntAgatha. % 0.55/0.85 % 0.55/0.85 % Refs : [FKK08] Fuchs et al. (2008), Attempto Controlled English for K % 0.55/0.85 % Source : [TPTP] % 0.55/0.85 % Names : % 0.55/0.85 % 0.55/0.85 % Status : Theorem % 0.55/0.85 % Rating : 0.31 v8.1.0, 0.25 v7.5.0, 0.28 v7.4.0, 0.23 v7.3.0, 0.17 v7.2.0, 0.14 v7.1.0, 0.17 v6.4.0, 0.19 v6.3.0, 0.21 v6.2.0, 0.32 v6.1.0, 0.37 v6.0.0, 0.39 v5.5.0, 0.37 v5.4.0, 0.39 v5.3.0, 0.52 v5.2.0, 0.25 v5.1.0, 0.29 v5.0.0, 0.38 v4.1.0, 0.48 v4.0.1, 0.52 v4.0.0 % 0.55/0.85 % Syntax : Number of formulae : 2 ( 1 unt; 0 def) % 0.55/0.85 % Number of atoms : 38 ( 7 equ) % 0.55/0.85 % Maximal formula atoms : 37 ( 19 avg) % 0.55/0.85 % Number of connectives : 43 ( 7 ~; 2 |; 24 &) % 0.55/0.85 % ( 0 <=>; 10 =>; 0 <=; 0 <~>) % 0.55/0.85 % Maximal formula depth : 23 ( 13 avg) % 0.55/0.85 % Maximal term depth : 1 ( 1 avg) % 0.55/0.85 % Number of predicates : 6 ( 4 usr; 1 prp; 0-4 aty) % 0.55/0.85 % Number of functors : 10 ( 10 usr; 10 con; 0-0 aty) % 0.55/0.85 % Number of variables : 29 ( 14 !; 15 ?) % 0.55/0.85 % SPC : FOF_THM_RFO_SEQ % 0.55/0.85 % 0.55/0.85 % Comments : % 0.55/0.85 %------------------------------------------------------------------------------ % 0.55/0.85 fof(background,axiom, % 0.55/0.85 ? [A,B,C] : % 0.55/0.85 ( $true % 0.55/0.85 & predicate1(B,live,A) % 0.55/0.85 & modifier_pp(B,in,'DreadburyMansion') % 0.55/0.85 & predicate2(C,kill,A,'AuntAgatha') % 0.55/0.85 & ! [D,E] : % 0.55/0.85 ( ( $true % 0.55/0.85 & predicate1(E,live,D) % 0.55/0.85 & modifier_pp(E,in,'DreadburyMansion') ) % 0.55/0.85 => ( D = 'AuntAgatha' % 0.55/0.85 | D = 'Butler' % 0.55/0.85 | D = 'Charles' ) ) % 0.55/0.85 & ! [F] : % 0.55/0.85 ( $true % 0.55/0.85 => ! [G,H] : % 0.55/0.85 ( ( $true % 0.55/0.85 & predicate2(H,kill,F,G) ) % 0.55/0.85 => ? [I] : predicate2(I,hate,F,G) ) ) % 0.55/0.85 & ! [J] : % 0.55/0.85 ( $true % 0.55/0.85 => ~ ? [K,L,M] : % 0.55/0.85 ( $true % 0.55/0.85 & predicate2(L,kill,J,K) % 0.55/0.85 & property2(M,rich,comp_than,K) % 0.55/0.85 & J = M ) ) % 0.55/0.85 & ! [N,O] : % 0.55/0.85 ( ( $true % 0.55/0.85 & predicate2(O,hate,'AuntAgatha',N) ) % 0.55/0.85 => ~ ? [P] : predicate2(P,hate,'Charles',N) ) % 0.55/0.85 & ~ ? [Q] : predicate2(Q,hate,'AuntAgatha','Butler') % 0.55/0.85 & ! [R] : % 0.55/0.85 ( ( $true % 0.55/0.85 & R != 'Butler' ) % 0.55/0.85 => ? [S] : predicate2(S,hate,'AuntAgatha',R) ) % 0.55/0.85 & ! [T] : % 0.55/0.85 ( ( $true % 0.55/0.85 & ~ ? [U] : % 0.55/0.85 ( property2(U,rich,comp_than,'AuntAgatha') % 0.55/0.85 & T = U ) ) % 0.55/0.85 => ? [V] : predicate2(V,hate,'Butler',T) ) % 0.55/0.85 & ! [W,X] : % 0.55/0.85 ( ( $true % 0.55/0.85 & predicate2(X,hate,'AuntAgatha',W) ) % 0.55/0.85 => ? [Y] : predicate2(Y,hate,'Butler',W) ) % 0.55/0.85 & ! [Z] : % 0.55/0.85 ( $true % 0.55/0.85 => ~ ! [A1] : % 0.55/0.85 ( $true % 0.55/0.85 => ? [B1] : predicate2(B1,hate,Z,A1) ) ) % 0.55/0.85 & 'AuntAgatha' != 'Butler' ) ). % 0.55/0.85 % 0.55/0.85 fof(prove,conjecture, % 0.55/0.85 ? [A] : predicate2(A,kill,'AuntAgatha','AuntAgatha') ). % 0.55/0.85 % 0.55/0.85 %------------------------------------------------------------------------------ % 0.55/0.85 %------------------------------------------- % 0.55/0.85 % Proof found % 0.55/0.85 % SZS status Theorem for theBenchmark % 0.55/0.85 % SZS output start Proof % 0.55/0.85 %ClaNum:39(EqnAxiom:24) % 0.55/0.85 %VarNum:43(SingletonVarNum:21) % 0.55/0.85 %MaxLitNum:5 % 0.55/0.85 %MaxfuncDepth:1 % 0.55/0.85 %SharedTerms:17 % 0.55/0.85 %goalClause: 29 % 0.55/0.85 %singleGoalClaCount:1 % 0.55/0.85 [25]P1(a1,a8,a2) % 0.55/0.85 [26]P2(a1,a9,a3) % 0.55/0.85 [27]P3(a10,a18,a2,a4) % 0.55/0.85 [28]~E(a5,a4) % 0.55/0.85 [29]~P3(x291,a18,a4,a4) % 0.55/0.85 [30]~P3(x301,a11,a4,a5) % 0.55/0.85 [31]~P3(x311,a11,x312,f12(x312)) % 0.55/0.85 [33]E(x331,a5)+P3(f13(x331),a11,a4,x331) % 0.55/0.85 [34]E(f15(x341),x341)+P3(f16(x341),a11,a5,x341) % 0.55/0.85 [35]P3(f16(x351),a11,a5,x351)+P4(f15(x351),a19,a7,a4) % 0.55/0.85 [36]~P3(x362,a11,a4,x361)+P3(f17(x361),a11,a5,x361) % 0.55/0.85 [38]~P3(x381,a11,a6,x382)+~P3(x383,a11,a4,x382) % 0.55/0.85 [37]~P3(x373,a18,x371,x372)+P3(f14(x371,x372),a11,x371,x372) % 0.55/0.85 [39]~E(x391,x392)+~P3(x393,a18,x391,x394)+~P4(x392,a19,a7,x394) % 0.55/0.85 [32]~P1(x322,a8,x321)+E(x321,a5)+E(x321,a6)+E(x321,a4)+~P2(x322,a9,a3) % 0.55/0.85 %EqnAxiom % 0.55/0.85 [1]E(x11,x11) % 0.55/0.85 [2]E(x22,x21)+~E(x21,x22) % 0.55/0.85 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.55/0.85 [4]~E(x41,x42)+E(f12(x41),f12(x42)) % 0.55/0.85 [5]~E(x51,x52)+E(f13(x51),f13(x52)) % 0.55/0.85 [6]~E(x61,x62)+E(f15(x61),f15(x62)) % 0.55/0.85 [7]~E(x71,x72)+E(f16(x71),f16(x72)) % 0.55/0.85 [8]~E(x81,x82)+E(f17(x81),f17(x82)) % 0.55/0.85 [9]~E(x91,x92)+E(f14(x91,x93),f14(x92,x93)) % 0.55/0.85 [10]~E(x101,x102)+E(f14(x103,x101),f14(x103,x102)) % 0.55/0.85 [11]P1(x112,x113,x114)+~E(x111,x112)+~P1(x111,x113,x114) % 0.55/0.85 [12]P1(x123,x122,x124)+~E(x121,x122)+~P1(x123,x121,x124) % 0.55/0.85 [13]P1(x133,x134,x132)+~E(x131,x132)+~P1(x133,x134,x131) % 0.55/0.85 [14]P2(x142,x143,x144)+~E(x141,x142)+~P2(x141,x143,x144) % 0.55/0.85 [15]P2(x153,x152,x154)+~E(x151,x152)+~P2(x153,x151,x154) % 0.55/0.85 [16]P2(x163,x164,x162)+~E(x161,x162)+~P2(x163,x164,x161) % 0.55/0.85 [17]P3(x172,x173,x174,x175)+~E(x171,x172)+~P3(x171,x173,x174,x175) % 0.55/0.85 [18]P3(x183,x182,x184,x185)+~E(x181,x182)+~P3(x183,x181,x184,x185) % 0.55/0.85 [19]P3(x193,x194,x192,x195)+~E(x191,x192)+~P3(x193,x194,x191,x195) % 0.55/0.85 [20]P3(x203,x204,x205,x202)+~E(x201,x202)+~P3(x203,x204,x205,x201) % 0.55/0.85 [21]P4(x212,x213,x214,x215)+~E(x211,x212)+~P4(x211,x213,x214,x215) % 0.55/0.85 [22]P4(x223,x222,x224,x225)+~E(x221,x222)+~P4(x223,x221,x224,x225) % 0.55/0.85 [23]P4(x233,x234,x232,x235)+~E(x231,x232)+~P4(x233,x234,x231,x235) % 0.55/0.85 [24]P4(x243,x244,x245,x242)+~E(x241,x242)+~P4(x243,x244,x245,x241) % 0.55/0.85 % 0.55/0.85 %------------------------------------------- % 0.55/0.85 cnf(40,plain, % 0.55/0.85 (~P3(x402,a18,x401,x403)+~P4(x401,a19,a7,x403)), % 0.55/0.85 inference(equality_inference,[],[39])). % 0.55/0.85 cnf(41,plain, % 0.55/0.85 (E(f12(a4),a5)), % 0.55/0.85 inference(scs_inference,[],[31,33])). % 0.55/0.85 cnf(42,plain, % 0.55/0.85 (~P3(x421,a11,x422,f12(x422))), % 0.55/0.85 inference(rename_variables,[],[31])). % 0.55/0.85 cnf(44,plain, % 0.55/0.85 (E(f15(f12(a5)),f12(a5))), % 0.55/0.86 inference(scs_inference,[],[31,42,33,34])). % 0.55/0.86 cnf(45,plain, % 0.55/0.86 (~P3(x451,a11,x452,f12(x452))), % 0.55/0.86 inference(rename_variables,[],[31])). % 0.55/0.86 cnf(47,plain, % 0.55/0.86 (~P3(x471,a11,a4,f12(a5))), % 0.55/0.86 inference(scs_inference,[],[31,42,45,33,34,36])). % 0.55/0.86 cnf(54,plain, % 0.55/0.86 (~E(a2,a4)), % 0.55/0.86 inference(scs_inference,[],[29,30,31,42,45,27,33,34,36,37,2,19])). % 0.55/0.86 cnf(56,plain, % 0.55/0.86 (P3(x561,a18,a2,a4)+~E(a10,x561)), % 0.55/0.86 inference(scs_inference,[],[29,30,31,42,45,27,33,34,36,37,2,19,17])). % 0.55/0.86 cnf(66,plain, % 0.55/0.86 (E(f12(a5),a5)), % 0.55/0.86 inference(scs_inference,[],[47,33])). % 0.55/0.86 cnf(67,plain, % 0.55/0.86 (~P3(x671,a11,a4,f12(a5))), % 0.55/0.86 inference(rename_variables,[],[47])). % 0.55/0.86 cnf(73,plain, % 0.55/0.86 (E(f15(f12(a5)),a5)), % 0.55/0.86 inference(scs_inference,[],[44,47,67,33,2,37,3])). % 0.55/0.86 cnf(89,plain, % 0.55/0.86 (E(a5,f12(a5))), % 0.55/0.86 inference(scs_inference,[],[31,66,37,2])). % 0.55/0.86 cnf(92,plain, % 0.55/0.86 (E(a2,a5)+E(a2,a6)), % 0.55/0.86 inference(scs_inference,[],[54,31,41,66,27,26,25,37,2,20,3,32])). % 0.55/0.86 cnf(94,plain, % 0.55/0.86 (P1(a1,a8,a5)+E(a2,a6)), % 0.55/0.86 inference(scs_inference,[],[54,31,41,66,27,26,25,37,2,20,3,32,13])). % 0.55/0.86 cnf(96,plain, % 0.55/0.86 (E(a5,f15(f12(a5)))), % 0.55/0.86 inference(scs_inference,[],[73,2])). % 0.55/0.86 cnf(108,plain, % 0.55/0.86 (~P3(x1081,a18,a6,x1082)+~P3(x1083,a11,a4,x1082)), % 0.55/0.86 inference(scs_inference,[],[38,37])). % 0.55/0.86 cnf(109,plain, % 0.55/0.86 (~P4(a2,a19,a7,a4)+~E(a10,x1091)), % 0.55/0.86 inference(scs_inference,[],[40,56])). % 0.55/0.86 cnf(110,plain, % 0.55/0.86 (~P4(a2,a19,a7,a4)), % 0.55/0.86 inference(equality_inference,[],[109])). % 0.55/0.86 cnf(112,plain, % 0.55/0.86 (~E(a2,a6)+~P3(x1121,a11,a4,a4)), % 0.55/0.86 inference(scs_inference,[],[27,108,19])). % 0.55/0.86 cnf(113,plain, % 0.55/0.86 (E(a4,a5)+~E(a2,a6)), % 0.55/0.86 inference(scs_inference,[],[112,33])). % 0.55/0.86 cnf(114,plain, % 0.55/0.86 (~E(a2,a6)), % 0.55/0.86 inference(scs_inference,[],[28,113,2])). % 0.55/0.86 cnf(115,plain, % 0.55/0.86 (E(a2,a5)), % 0.55/0.86 inference(scs_inference,[],[114,92])). % 0.55/0.86 cnf(116,plain, % 0.55/0.86 (P1(a1,a8,a5)), % 0.55/0.86 inference(scs_inference,[],[114,94])). % 0.55/0.86 cnf(120,plain, % 0.55/0.86 (E(a2,f12(a5))), % 0.55/0.86 inference(scs_inference,[],[115,89,116,2,13,3])). % 0.55/0.86 cnf(128,plain, % 0.55/0.86 (E(a2,f15(f12(a5)))), % 0.55/0.86 inference(scs_inference,[],[115,96,120,116,2,13,3])). % 0.55/0.86 cnf(134,plain, % 0.55/0.86 (E(f15(f12(a5)),a2)), % 0.55/0.86 inference(scs_inference,[],[128,2])). % 0.55/0.86 cnf(173,plain, % 0.55/0.86 ($false), % 0.55/0.86 inference(scs_inference,[],[110,134,31,21,35]), % 0.55/0.86 ['proof']). % 0.55/0.86 % SZS output end Proof % 0.55/0.86 % Total time :0.240000s %------------------------------------------------------------------------------