%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM007+2 : TPTP v8.2.0. Released v3.2.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 04:52:43 EDT 2024 % Result : Theorem 1.02s 1.09s % Output : CNFRefutation 1.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : COM007+2 : TPTP v8.2.0. Released v3.2.0. % 0.00/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.29 % Computer : n024.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 300 % 0.09/0.29 % DateTime : Thu Jun 20 23:40:38 EDT 2024 % 0.09/0.29 % CPUTime : % 0.14/0.53 start to proof:theBenchmark % 1.02/1.08 %------------------------------------------- % 1.02/1.08 % File :CSE---1.7 % 1.02/1.08 % Problem :theBenchmark % 1.02/1.08 % Transform :cnf % 1.02/1.08 % Format :tptp:raw % 1.02/1.08 % Command :java -jar mcs_scs.jar %d %s % 1.02/1.08 % 1.02/1.08 % Result :Theorem 0.520000s % 1.02/1.08 % Output :CNFRefutation 0.520000s % 1.02/1.08 %------------------------------------------- % 1.02/1.09 %------------------------------------------------------------------------------ % 1.02/1.09 % File : COM007+2 : TPTP v8.2.0. Released v3.2.0. % 1.02/1.09 % Domain : Computing Theory % 1.02/1.09 % Problem : Preservation of the Diamond Property under reflexive closure % 1.02/1.09 % Version : Especial. % 1.02/1.09 % English : % 1.02/1.09 % 1.02/1.09 % Refs : [Bez05] Bezem (2005), Email to Geoff Sutcliffe % 1.02/1.09 % Source : [Bez05] % 1.02/1.09 % Names : dpe [Bez05] % 1.02/1.09 % 1.02/1.09 % Status : Theorem % 1.02/1.09 % Rating : 0.17 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.13 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.04 v6.2.0, 0.12 v6.1.0, 0.17 v5.5.0, 0.15 v5.4.0, 0.14 v5.3.0, 0.22 v5.2.0, 0.05 v5.0.0, 0.08 v4.1.0, 0.09 v4.0.0, 0.08 v3.7.0, 0.14 v3.5.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.00 v3.2.0 % 1.02/1.09 % 1.02/1.09 % Syntax : Number of formulae : 7 ( 1 unt; 0 def) % 1.02/1.09 % Number of atoms : 17 ( 2 equ) % 1.02/1.09 % Maximal formula atoms : 4 ( 2 avg) % 1.02/1.09 % Number of connectives : 10 ( 0 ~; 1 |; 4 &) % 1.02/1.09 % ( 0 <=>; 5 =>; 0 <=; 0 <~>) % 1.02/1.09 % Maximal formula depth : 7 ( 4 avg) % 1.02/1.09 % Maximal term depth : 1 ( 1 avg) % 1.02/1.09 % Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty) % 1.02/1.09 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 1.02/1.09 % Number of variables : 11 ( 10 !; 1 ?) % 1.02/1.09 % SPC : FOF_THM_RFO_SEQ % 1.02/1.09 % 1.02/1.09 % Comments : % 1.02/1.09 %------------------------------------------------------------------------------ % 1.02/1.09 fof(assumption,axiom, % 1.02/1.09 ( reflexive_rewrite(a,b) % 1.02/1.09 & reflexive_rewrite(a,c) ) ). % 1.02/1.09 % 1.02/1.09 fof(goal_ax,axiom, % 1.02/1.09 ! [A] : % 1.02/1.09 ( ( reflexive_rewrite(b,A) % 1.02/1.09 & reflexive_rewrite(c,A) ) % 1.02/1.09 => goal ) ). % 1.02/1.09 % 1.02/1.09 fof(equal_in_reflexive_rewrite,axiom, % 1.02/1.09 ! [A,B] : % 1.02/1.09 ( A = B % 1.02/1.09 => reflexive_rewrite(A,B) ) ). % 1.02/1.09 % 1.02/1.09 fof(rewrite_in_reflexive_rewrite,axiom, % 1.02/1.09 ! [A,B] : % 1.02/1.09 ( rewrite(A,B) % 1.02/1.09 => reflexive_rewrite(A,B) ) ). % 1.02/1.09 % 1.02/1.09 fof(equal_or_rewrite,axiom, % 1.02/1.09 ! [A,B] : % 1.02/1.09 ( reflexive_rewrite(A,B) % 1.02/1.09 => ( A = B % 1.02/1.09 | rewrite(A,B) ) ) ). % 1.02/1.09 % 1.02/1.09 fof(rewrite_diamond,axiom, % 1.02/1.09 ! [A,B,C] : % 1.02/1.09 ( ( rewrite(A,B) % 1.02/1.09 & rewrite(A,C) ) % 1.02/1.09 => ? [D] : % 1.02/1.09 ( rewrite(B,D) % 1.02/1.09 & rewrite(C,D) ) ) ). % 1.02/1.09 % 1.02/1.09 fof(goal_to_be_proved,conjecture, % 1.02/1.09 goal ). % 1.02/1.09 % 1.02/1.09 %------------------------------------------------------------------------------ % 1.02/1.09 %------------------------------------------- % 1.02/1.09 % Proof found % 1.02/1.09 % SZS status Theorem for theBenchmark % 1.02/1.09 % SZS output start Proof % 1.02/1.09 %ClaNum:20(EqnAxiom:11) % 1.02/1.09 %VarNum:32(SingletonVarNum:13) % 1.02/1.09 %MaxLitNum:3 % 1.02/1.09 %MaxfuncDepth:1 % 1.02/1.09 %SharedTerms:8 % 1.02/1.09 %goalClause: 14 % 1.02/1.09 %singleGoalClaCount:1 % 1.02/1.09 [12]P1(a1,a2) % 1.02/1.09 [13]P1(a1,a3) % 1.02/1.09 [14]~P2(a5000) % 1.02/1.09 [15]~E(x151,x152)+P1(x151,x152) % 1.02/1.09 [16]~P3(x161,x162)+P1(x161,x162) % 1.02/1.09 [18]~P1(a3,x181)+~P1(a2,x181)+P2(a5000) % 1.02/1.09 [17]P3(x171,x172)+~P1(x171,x172)+E(x171,x172) % 1.02/1.09 [19]~P3(x192,x193)+~P3(x192,x191)+P3(x191,f4(x192,x193,x191)) % 1.02/1.09 [20]~P3(x202,x203)+~P3(x202,x201)+P3(x201,f4(x202,x201,x203)) % 1.02/1.09 %EqnAxiom % 1.02/1.09 [1]E(x11,x11) % 1.02/1.09 [2]E(x22,x21)+~E(x21,x22) % 1.02/1.09 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.02/1.09 [4]~E(x41,x42)+E(f4(x41,x43,x44),f4(x42,x43,x44)) % 1.02/1.09 [5]~E(x51,x52)+E(f4(x53,x51,x54),f4(x53,x52,x54)) % 1.02/1.09 [6]~E(x61,x62)+E(f4(x63,x64,x61),f4(x63,x64,x62)) % 1.02/1.09 [7]P1(x72,x73)+~E(x71,x72)+~P1(x71,x73) % 1.02/1.09 [8]P1(x83,x82)+~E(x81,x82)+~P1(x83,x81) % 1.02/1.09 [9]P3(x92,x93)+~E(x91,x92)+~P3(x91,x93) % 1.02/1.09 [10]P3(x103,x102)+~E(x101,x102)+~P3(x103,x101) % 1.02/1.09 [11]~P2(x111)+P2(x112)+~E(x111,x112) % 1.02/1.09 % 1.02/1.09 %------------------------------------------- % 1.02/1.09 cnf(21,plain, % 1.02/1.09 (P1(x211,x211)), % 1.02/1.09 inference(equality_inference,[],[15])). % 1.02/1.09 cnf(23,plain, % 1.02/1.09 (P1(x231,x231)), % 1.02/1.09 inference(rename_variables,[],[21])). % 1.02/1.09 cnf(26,plain, % 1.02/1.09 (P1(x261,x261)), % 1.02/1.09 inference(rename_variables,[],[21])). % 1.02/1.09 cnf(29,plain, % 1.02/1.09 (~P3(a3,a2)), % 1.02/1.09 inference(scs_inference,[],[14,21,23,26,18,7,8,16])). % 1.02/1.09 cnf(31,plain, % 1.02/1.09 (E(a1,a2)+P3(a1,a2)), % 1.02/1.09 inference(scs_inference,[],[14,21,23,26,12,18,7,8,16,17])). % 1.02/1.09 cnf(36,plain, % 1.02/1.09 (~P1(a2,x361)+~P1(a3,x361)), % 1.02/1.09 inference(scs_inference,[],[14,18])). % 1.02/1.09 cnf(43,plain, % 1.02/1.09 (P3(a1,a2)), % 1.02/1.09 inference(scs_inference,[],[21,13,36,16,7,31])). % 1.02/1.09 cnf(46,plain, % 1.02/1.09 (P3(a1,a3)), % 1.02/1.09 inference(scs_inference,[],[29,21,13,36,16,7,31,9,10,17])). % 1.02/1.09 cnf(51,plain, % 1.02/1.09 (P3(a1,x511)+~E(a3,x511)), % 1.02/1.09 inference(scs_inference,[],[46,10])). % 1.02/1.09 cnf(129,plain, % 1.02/1.09 (~E(a3,x1291)+P3(a2,f4(a1,a2,x1291))), % 1.02/1.09 inference(scs_inference,[],[43,51,20])). % 1.02/1.09 cnf(134,plain, % 1.02/1.09 (~E(a3,x1341)+P3(x1341,f4(a1,a2,x1341))), % 1.02/1.09 inference(scs_inference,[],[43,51,19])). % 1.02/1.09 cnf(236,plain, % 1.02/1.09 (P1(a2,f4(a1,a2,x2361))+~E(a3,x2361)), % 1.02/1.09 inference(scs_inference,[],[129,16])). % 1.02/1.09 cnf(237,plain, % 1.02/1.09 (P1(a2,f4(a1,a2,a3))), % 1.02/1.09 inference(equality_inference,[],[236])). % 1.02/1.09 cnf(264,plain, % 1.02/1.09 (P1(x2641,f4(a1,a2,x2641))+~E(a3,x2641)), % 1.02/1.09 inference(scs_inference,[],[134,16])). % 1.02/1.09 cnf(265,plain, % 1.02/1.09 (P1(a3,f4(a1,a2,a3))), % 1.02/1.09 inference(equality_inference,[],[264])). % 1.02/1.09 cnf(266,plain, % 1.02/1.09 ($false), % 1.02/1.09 inference(scs_inference,[],[237,265,36]), % 1.02/1.09 ['proof']). % 1.02/1.09 % SZS output end Proof % 1.02/1.09 % Total time :0.520000s %------------------------------------------------------------------------------