%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV014-1 : TPTP v8.2.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n020.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 16:45:29 EDT 2024 % Result : Unsatisfiable 123.55s 123.63s % Output : CNFRefutation 123.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : SWV014-1 : TPTP v8.2.0. Released v2.4.0. % 0.04/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n020.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Jun 20 19:28:39 EDT 2024 % 0.12/0.34 % CPUTime : % 0.52/0.58 start to proof:theBenchmark % 123.55/123.60 %------------------------------------------- % 123.55/123.60 % File :CSE---1.7 % 123.55/123.60 % Problem :theBenchmark % 123.55/123.60 % Transform :cnf % 123.55/123.60 % Format :tptp:raw % 123.55/123.60 % Command :java -jar mcs_scs.jar %d %s % 123.55/123.60 % 123.55/123.60 % Result :Theorem 122.930000s % 123.55/123.60 % Output :CNFRefutation 122.930000s % 123.55/123.60 %------------------------------------------- % 123.55/123.62 %-------------------------------------------------------------------------- % 123.55/123.62 % File : SWV014-1 : TPTP v8.2.0. Released v2.4.0. % 123.55/123.62 % Domain : Software Verification % 123.55/123.62 % Problem : Fact 6 of the Neumann-Stubblebine analysis % 123.55/123.62 % Version : [Wei99] axioms. % 123.55/123.62 % English : % 123.55/123.62 % 123.55/123.62 % Refs : [Wei99] Weidenbach (1999), Towards and Automatic Analysis of S % 123.55/123.62 % [Bau99] Baumgartner (1999), FTP'2000 - Problem Sets % 123.55/123.62 % Source : [TPTP] % 123.55/123.62 % Names : % 123.55/123.62 % 123.55/123.62 % Status : Unsatisfiable % 123.55/123.62 % Rating : 0.36 v8.2.0, 0.43 v8.1.0, 0.50 v6.1.0, 0.64 v6.0.0, 0.56 v5.5.0, 0.62 v5.4.0, 0.61 v5.3.0, 0.65 v5.2.0, 0.69 v5.1.0, 0.62 v5.0.0, 0.53 v4.1.0, 0.60 v4.0.1, 0.71 v3.7.0, 0.57 v3.4.0, 0.40 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.38 v2.6.0, 0.14 v2.5.0, 0.57 v2.4.0 % 123.55/123.62 % Syntax : Number of clauses : 34 ( 11 unt; 0 nHn; 32 RR) % 123.55/123.62 % Number of literals : 77 ( 0 equ; 44 neg) % 123.55/123.62 % Maximal clause size : 5 ( 2 avg) % 123.55/123.62 % Maximal term depth : 6 ( 1 avg) % 123.55/123.62 % Number of predicates : 10 ( 10 usr; 0 prp; 1-1 aty) % 123.55/123.62 % Number of functors : 15 ( 15 usr; 6 con; 0-4 aty) % 123.55/123.62 % Number of variables : 75 ( 26 sgn) % 123.55/123.62 % SPC : CNF_UNS_RFO_NEQ_HRN % 123.55/123.62 % 123.55/123.62 % Comments : Created by tptp2X -f tptp -t cnf:otter SWV014+1.p % 123.55/123.62 %-------------------------------------------------------------------------- % 123.55/123.62 cnf(a_is_party_of_protocol_2,axiom, % 123.55/123.62 party_of_protocol(a) ). % 123.55/123.62 % 123.55/123.62 cnf(a_sent_message_i_to_b_3,axiom, % 123.55/123.62 message(sent(a,b,pair(a,an_a_nonce))) ). % 123.55/123.63 % 123.55/123.63 cnf(a_stored_message_i_4,axiom, % 123.55/123.63 a_stored(pair(b,an_a_nonce)) ). % 123.55/123.63 % 123.55/123.63 cnf(a_forwards_secure_5,axiom, % 123.55/123.63 ( message(sent(a,A,pair(E,encrypt(F,C)))) % 123.55/123.63 | ~ a_stored(pair(A,B)) % 123.55/123.63 | ~ message(sent(t,a,triple(encrypt(quadruple(A,B,C,D),at),E,F))) ) ). % 123.55/123.63 % 123.55/123.63 cnf(b_is_party_of_protocol_8,axiom, % 123.55/123.63 party_of_protocol(b) ). % 123.55/123.63 % 123.55/123.63 cnf(nonce_a_is_fresh_to_b_9,axiom, % 123.55/123.63 fresh_to_b(an_a_nonce) ). % 123.55/123.63 % 123.55/123.63 cnf(b_creates_freash_nonces_in_time_10,axiom, % 123.55/123.63 ( message(sent(b,t,triple(b,generate_b_nonce(B),encrypt(triple(A,B,generate_expiration_time(B)),bt)))) % 123.55/123.63 | ~ fresh_to_b(B) % 123.55/123.63 | ~ message(sent(A,b,pair(A,B))) ) ). % 123.55/123.63 % 123.55/123.63 cnf(b_creates_freash_nonces_in_time_11,axiom, % 123.55/123.63 ( b_stored(pair(A,B)) % 123.55/123.63 | ~ fresh_to_b(B) % 123.55/123.63 | ~ message(sent(A,b,pair(A,B))) ) ). % 123.55/123.63 % 123.55/123.63 cnf(b_accepts_secure_session_key_12,axiom, % 123.55/123.63 ( b_holds(key(B,A)) % 123.55/123.63 | ~ b_stored(pair(A,C)) % 123.55/123.63 | ~ message(sent(A,b,pair(encrypt(triple(A,B,generate_expiration_time(C)),bt),encrypt(generate_b_nonce(C),B)))) ) ). % 123.55/123.63 % 123.55/123.63 cnf(t_holds_key_at_for_a_13,axiom, % 123.55/123.63 t_holds(key(at,a)) ). % 123.55/123.63 % 123.55/123.63 cnf(t_holds_key_bt_for_b_14,axiom, % 123.55/123.63 t_holds(key(bt,b)) ). % 123.55/123.63 % 123.55/123.63 cnf(t_is_party_of_protocol_15,axiom, % 123.55/123.63 party_of_protocol(t) ). % 123.55/123.63 % 123.55/123.63 cnf(server_t_generates_key_16,axiom, % 123.55/123.63 ( message(sent(t,C,triple(encrypt(quadruple(A,D,generate_key(D),E),G),encrypt(triple(C,generate_key(D),E),F),B))) % 123.55/123.63 | ~ a_nonce(D) % 123.55/123.63 | ~ message(sent(A,t,triple(A,B,encrypt(triple(C,D,E),F)))) % 123.55/123.63 | ~ t_holds(key(G,C)) % 123.55/123.63 | ~ t_holds(key(F,A)) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_can_record_17,axiom, % 123.55/123.63 ( intruder_message(C) % 123.55/123.63 | ~ message(sent(A,B,C)) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_decomposes_pairs_18,axiom, % 123.55/123.63 ( intruder_message(A) % 123.55/123.63 | ~ intruder_message(pair(A,B)) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_decomposes_pairs_19,axiom, % 123.55/123.63 ( intruder_message(B) % 123.55/123.63 | ~ intruder_message(pair(A,B)) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_decomposes_triples_20,axiom, % 123.55/123.63 ( intruder_message(A) % 123.55/123.63 | ~ intruder_message(triple(A,B,C)) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_decomposes_triples_21,axiom, % 123.55/123.63 ( intruder_message(B) % 123.55/123.63 | ~ intruder_message(triple(A,B,C)) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_decomposes_triples_22,axiom, % 123.55/123.63 ( intruder_message(C) % 123.55/123.63 | ~ intruder_message(triple(A,B,C)) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_decomposes_quadruples_23,axiom, % 123.55/123.63 ( intruder_message(A) % 123.55/123.63 | ~ intruder_message(quadruple(A,B,C,D)) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_decomposes_quadruples_24,axiom, % 123.55/123.63 ( intruder_message(B) % 123.55/123.63 | ~ intruder_message(quadruple(A,B,C,D)) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_decomposes_quadruples_25,axiom, % 123.55/123.63 ( intruder_message(C) % 123.55/123.63 | ~ intruder_message(quadruple(A,B,C,D)) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_decomposes_quadruples_26,axiom, % 123.55/123.63 ( intruder_message(D) % 123.55/123.63 | ~ intruder_message(quadruple(A,B,C,D)) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_composes_pairs_27,axiom, % 123.55/123.63 ( intruder_message(pair(A,B)) % 123.55/123.63 | ~ intruder_message(B) % 123.55/123.63 | ~ intruder_message(A) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_composes_triples_28,axiom, % 123.55/123.63 ( intruder_message(triple(A,B,C)) % 123.55/123.63 | ~ intruder_message(C) % 123.55/123.63 | ~ intruder_message(B) % 123.55/123.63 | ~ intruder_message(A) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_composes_quadruples_29,axiom, % 123.55/123.63 ( intruder_message(quadruple(A,B,C,D)) % 123.55/123.63 | ~ intruder_message(D) % 123.55/123.63 | ~ intruder_message(C) % 123.55/123.63 | ~ intruder_message(B) % 123.55/123.63 | ~ intruder_message(A) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_interception_30,axiom, % 123.55/123.63 ( intruder_message(B) % 123.55/123.63 | ~ intruder_holds(key(B,C)) % 123.55/123.63 | ~ intruder_message(encrypt(A,B)) % 123.55/123.63 | ~ party_of_protocol(C) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_message_sent_31,axiom, % 123.55/123.63 ( message(sent(B,C,A)) % 123.55/123.63 | ~ intruder_message(A) % 123.55/123.63 | ~ party_of_protocol(C) % 123.55/123.63 | ~ party_of_protocol(B) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_holds_key_32,axiom, % 123.55/123.63 ( intruder_holds(key(A,B)) % 123.55/123.63 | ~ intruder_message(A) % 123.55/123.63 | ~ party_of_protocol(B) ) ). % 123.55/123.63 % 123.55/123.63 cnf(intruder_key_encrypts_33,axiom, % 123.55/123.63 ( intruder_message(encrypt(A,B)) % 123.55/123.63 | ~ intruder_holds(key(B,C)) % 123.55/123.63 | ~ intruder_message(A) % 123.55/123.63 | ~ party_of_protocol(C) ) ). % 123.55/123.63 % 123.55/123.63 cnf(an_a_nonce_is_a_nonce_34,axiom, % 123.55/123.63 a_nonce(an_a_nonce) ). % 123.55/123.63 % 123.55/123.63 cnf(generated_times_and_nonces_are_nonces_36,axiom, % 123.55/123.63 a_nonce(generate_expiration_time(A)) ). % 123.55/123.63 % 123.55/123.63 cnf(generated_times_and_nonces_are_nonces_37,axiom, % 123.55/123.63 a_nonce(generate_b_nonce(A)) ). % 123.55/123.63 % 123.55/123.63 cnf(co1_38,negated_conjecture, % 123.55/123.63 ( ~ b_holds(key(A,a)) % 123.55/123.63 | ~ intruder_holds(key(A,b)) ) ). % 123.55/123.63 % 123.55/123.63 %-------------------------------------------------------------------------- % 123.55/123.63 %------------------------------------------- % 123.55/123.63 % Proof found % 123.55/123.63 % SZS status Theorem for theBenchmark % 123.55/123.63 % SZS output start Proof % 123.55/123.65 %ClaNum:34(EqnAxiom:0) % 123.55/123.65 %VarNum:145(SingletonVarNum:75) % 123.55/123.65 %MaxLitNum:5 % 123.55/123.65 %MaxfuncDepth:5 % 123.55/123.65 %SharedTerms:20 % 123.55/123.65 %goalClause: 16 % 123.55/123.65 [1]P1(a1) % 123.55/123.65 [2]P1(a2) % 123.55/123.65 [3]P1(a5) % 123.55/123.65 [4]P2(a3) % 123.55/123.65 [5]P3(a3) % 123.55/123.65 [8]P4(f10(a2,a3)) % 123.55/123.65 [9]P10(f11(a4,a1)) % 123.55/123.65 [10]P10(f11(a7,a2)) % 123.55/123.65 [11]P7(f13(a1,a2,f10(a1,a3))) % 123.55/123.65 [6]P3(f6(x61)) % 123.55/123.65 [7]P3(f9(x71)) % 123.55/123.65 [16]~P9(f11(x161,a2))+~P5(f11(x161,a1)) % 123.55/123.65 [14]P8(x141)+~P8(f10(x142,x141)) % 123.55/123.65 [15]P8(x151)+~P8(f10(x151,x152)) % 123.55/123.65 [21]P8(x211)+~P7(f13(x212,x213,x211)) % 123.55/123.65 [22]P8(x221)+~P8(f15(x222,x223,x221)) % 123.55/123.65 [23]P8(x231)+~P8(f15(x232,x231,x233)) % 123.55/123.65 [24]P8(x241)+~P8(f15(x241,x242,x243)) % 123.55/123.65 [27]P8(x271)+~P8(f14(x272,x273,x274,x271)) % 123.55/123.65 [28]P8(x281)+~P8(f14(x282,x283,x281,x284)) % 123.55/123.65 [29]P8(x291)+~P8(f14(x292,x291,x293,x294)) % 123.55/123.65 [30]P8(x301)+~P8(f14(x301,x302,x303,x304)) % 123.55/123.65 [12]~P8(x122)+~P8(x121)+P8(f10(x121,x122)) % 123.55/123.65 [13]~P1(x132)+~P8(x131)+P9(f11(x131,x132)) % 123.55/123.65 [25]~P2(x252)+P6(f10(x251,x252))+~P7(f13(x251,a2,f10(x251,x252))) % 123.55/123.65 [31]~P2(x311)+~P7(f13(x312,a2,f10(x312,x311)))+P7(f13(a2,a5,f15(a2,f6(x311),f8(f15(x312,x311,f9(x311)),a7)))) % 123.55/123.65 [32]P5(f11(x321,x322))+~P6(f10(x322,x323))+~P7(f13(x322,a2,f10(f8(f15(x322,x321,f9(x323)),a7),f8(f6(x323),x321)))) % 123.55/123.65 [33]~P4(f10(x331,x335))+P7(f13(a1,x331,f10(x332,f8(x333,x334))))+~P7(f13(a5,a1,f15(f8(f14(x331,x335,x334,x336),a4),x332,x333))) % 123.55/123.65 [17]~P8(x171)+~P1(x173)+~P9(f11(x172,x173))+P8(f8(x171,x172)) % 123.55/123.65 [18]P8(x181)+~P1(x182)+~P9(f11(x181,x182))+~P8(f8(x183,x181)) % 123.55/123.65 [19]~P1(x192)+~P1(x191)+~P8(x193)+P7(f13(x191,x192,x193)) % 123.55/123.65 [20]~P8(x203)+~P8(x202)+~P8(x201)+P8(f15(x201,x202,x203)) % 123.55/123.65 [26]~P8(x264)+~P8(x263)+~P8(x262)+~P8(x261)+P8(f14(x261,x262,x263,x264)) % 123.55/123.65 [34]~P3(x343)+~P10(f11(x346,x342))+~P10(f11(x345,x341))+~P7(f13(x342,a5,f15(x342,x347,f8(f15(x341,x343,x344),x346))))+P7(f13(a5,x341,f15(f8(f14(x342,x343,f12(x343),x344),x345),f8(f15(x341,f12(x343),x344),x346),x347))) % 123.55/123.65 %EqnAxiom % 123.55/123.65 % 123.55/123.65 %------------------------------------------- % 123.55/123.67 cnf(35,plain, % 123.55/123.67 (P8(f10(a1,a3))), % 123.55/123.67 inference(scs_inference,[],[11,21])). % 123.55/123.67 cnf(37,plain, % 123.55/123.67 (P6(f10(a1,a3))), % 123.55/123.67 inference(scs_inference,[],[11,4,21,25])). % 123.55/123.67 cnf(39,plain, % 123.55/123.67 (P8(a3)), % 123.55/123.67 inference(scs_inference,[],[11,4,21,25,14])). % 123.55/123.67 cnf(43,plain, % 123.55/123.68 (P8(x431)+~P8(f15(x432,x433,f10(x434,x431)))), % 123.55/123.68 inference(scs_inference,[],[22,14])). % 123.55/123.68 cnf(44,plain, % 123.55/123.68 (P8(x441)+~P8(f15(x442,f10(x441,x443),x444))), % 123.55/123.68 inference(scs_inference,[],[23,15])). % 123.55/123.68 cnf(45,plain, % 123.55/123.68 (P8(x451)+~P8(f15(f14(x452,x453,x454,x451),x455,x456))), % 123.55/123.68 inference(scs_inference,[],[24,27])). % 123.55/123.68 cnf(46,plain, % 123.55/123.68 (~P9(f11(x461,a2))+~P7(f13(a1,a2,f10(f8(f15(a1,x461,f9(a3)),a7),f8(f6(a3),x461))))), % 123.55/123.68 inference(scs_inference,[],[37,16,32])). % 123.55/123.68 cnf(47,plain, % 123.55/123.68 (P8(x471)+~P8(f14(x472,x473,f14(x474,x471,x475,x476),x477))), % 123.55/123.68 inference(scs_inference,[],[28,29])). % 123.55/123.68 cnf(48,plain, % 123.55/123.68 (P8(x481)+~P8(f14(f15(x482,x483,f10(x484,x481)),x485,x486,x487))), % 123.55/123.68 inference(scs_inference,[],[30,43])). % 123.55/123.68 cnf(53,plain, % 123.55/123.68 (~P7(f13(a1,a2,f10(f8(f15(a1,f10(a1,a3),f9(a3)),a7),f8(f6(a3),f10(a1,a3)))))), % 123.55/123.68 inference(scs_inference,[],[2,35,46,13])). % 123.55/123.68 cnf(72,plain, % 123.55/123.68 (~P8(f6(a3))+~P8(f8(f15(a1,f10(a1,a3),f9(a3)),a7))+~P9(f11(f10(a1,a3),a1))), % 123.55/123.68 inference(scs_inference,[],[35,53,1,2,19,43,44,45,47,12,20,26,48,17])). % 123.55/123.68 cnf(90,plain, % 123.55/123.68 (~P8(f8(f15(a1,f10(a1,a3),f9(a3)),a7))+~P8(f6(a3))), % 123.55/123.68 inference(scs_inference,[],[1,35,72,13])). % 123.55/123.68 cnf(91,plain, % 123.55/123.68 (~P8(f6(a3))+~P8(f10(x911,f8(f15(a1,f10(a1,a3),f9(a3)),a7)))), % 123.55/123.68 inference(scs_inference,[],[90,14])). % 123.55/123.68 cnf(92,plain, % 123.55/123.68 (~P8(f6(a3))+~P8(f10(f10(x921,f8(f15(a1,f10(a1,a3),f9(a3)),a7)),x922))), % 123.55/123.68 inference(scs_inference,[],[91,15])). % 123.55/123.68 cnf(94,plain, % 123.55/123.68 (P7(f13(a2,a5,f15(a2,f6(a3),f8(f15(a1,a3,f9(a3)),a7))))), % 123.55/123.68 inference(scs_inference,[],[4,2,1,35,31,19])). % 123.55/123.68 cnf(97,plain, % 123.55/123.68 (P8(f8(f15(a1,a3,f9(a3)),a7))), % 123.55/123.68 inference(scs_inference,[],[94,21,22])). % 123.55/123.68 cnf(99,plain, % 123.55/123.68 (P8(f6(a3))), % 123.55/123.68 inference(scs_inference,[],[94,21,22,23])). % 123.55/123.68 cnf(101,plain, % 123.55/123.68 (P8(a2)), % 123.55/123.68 inference(scs_inference,[],[94,21,22,23,24])). % 123.55/123.68 cnf(103,plain, % 123.55/123.68 (~P8(f8(f15(a1,f10(a1,a3),f9(a3)),a7))), % 123.55/123.68 inference(scs_inference,[],[94,21,22,23,24,90])). % 123.55/123.68 cnf(104,plain, % 123.55/123.68 (~P8(f10(x1041,f8(f15(a1,f10(a1,a3),f9(a3)),a7)))), % 123.55/123.68 inference(scs_inference,[],[94,21,22,23,24,90,91])). % 123.55/123.68 cnf(105,plain, % 123.55/123.68 (~P8(f10(f10(x1051,f8(f15(a1,f10(a1,a3),f9(a3)),a7)),x1052))), % 123.55/123.68 inference(scs_inference,[],[94,21,22,23,24,90,91,92])). % 123.55/123.68 cnf(116,plain, % 123.55/123.68 (~P8(f10(f8(f15(a1,f10(a1,a3),f9(a3)),a7),x1161))), % 123.55/123.68 inference(scs_inference,[],[1,35,94,21,22,23,24,90,91,92,43,44,45,47,17,20])). % 123.55/123.68 cnf(118,plain, % 123.55/123.68 (~P8(f14(x1181,f8(f15(a1,f10(a1,a3),f9(a3)),a7),x1182,x1183))), % 123.55/123.68 inference(scs_inference,[],[1,35,94,21,22,23,24,90,91,92,43,44,45,47,17,20,26])). % 123.55/123.68 cnf(144,plain, % 123.55/123.68 (~P8(f10(x1441,f14(x1442,x1443,f8(f15(a1,f10(a1,a3),f9(a3)),a7),x1444)))), % 123.55/123.68 inference(scs_inference,[],[103,14,28])). % 123.55/123.68 cnf(149,plain, % 123.55/123.68 (~P8(f10(x1491,f14(f8(f15(a1,f10(a1,a3),f9(a3)),a7),x1492,x1493,x1494)))), % 123.55/123.68 inference(scs_inference,[],[103,14,30])). % 123.55/123.68 cnf(183,plain, % 123.55/123.68 (~P8(f10(x1831,f15(x1832,x1833,f8(f15(a1,f10(a1,a3),f9(a3)),a7))))), % 123.55/123.68 inference(scs_inference,[],[103,14,22])). % 123.55/123.68 cnf(184,plain, % 123.55/123.68 (~P8(f15(x1841,x1842,f8(f15(a1,f10(a1,a3),f9(a3)),a7)))), % 123.55/123.68 inference(scs_inference,[],[35,183,12])). % 123.55/123.68 cnf(188,plain, % 123.55/123.68 (~P8(f10(x1881,f15(f8(f15(a1,f10(a1,a3),f9(a3)),a7),x1882,x1883)))), % 123.55/123.68 inference(scs_inference,[],[103,14,24])). % 123.55/123.68 cnf(189,plain, % 123.55/123.68 (~P8(f15(f8(f15(a1,f10(a1,a3),f9(a3)),a7),x1891,x1892))), % 123.55/123.68 inference(scs_inference,[],[35,188,12])). % 123.55/123.68 cnf(214,plain, % 123.55/123.68 (P9(f11(a3,a1))), % 123.55/123.68 inference(scs_inference,[],[35,1,14,13])). % 123.55/123.68 cnf(223,plain, % 123.55/123.68 (~P8(f10(x2231,f14(x2232,f14(x2233,f8(f15(a1,f10(a1,a3),f9(a3)),a7),x2234,x2235),x2236,x2237)))), % 123.55/123.68 inference(scs_inference,[],[118,14,29])). % 123.55/123.68 cnf(231,plain, % 123.55/123.68 (P8(f8(a3,a3))), % 123.55/123.68 inference(scs_inference,[],[35,214,1,14,17])). % 123.55/123.68 cnf(318,plain, % 123.55/123.68 (P9(f11(a1,a5))), % 123.55/123.68 inference(scs_inference,[],[35,3,15,13])). % 123.55/123.68 cnf(321,plain, % 123.55/123.68 (P9(f11(a1,a1))), % 123.55/123.68 inference(scs_inference,[],[35,1,15,13])). % 123.55/123.68 cnf(322,plain, % 123.55/123.68 (P8(f8(a1,a3))), % 123.55/123.68 inference(scs_inference,[],[35,214,1,15,17])). % 123.55/123.68 cnf(325,plain, % 123.67/123.68 (~P7(f13(a5,a1,f15(f8(f14(a2,a3,a7,x3251),a4),x3252,f15(a1,f10(a1,a3),f9(a3)))))), % 123.67/123.68 inference(scs_inference,[],[104,8,21,33])). % 123.67/123.68 cnf(326,plain, % 123.67/123.68 (~P8(f15(f8(f14(a2,a3,a7,x3261),a4),x3262,f15(a1,f10(a1,a3),f9(a3))))), % 123.67/123.68 inference(scs_inference,[],[1,325,3,19])). % 123.67/123.68 cnf(416,plain, % 123.67/123.68 (P8(f8(f10(a1,a3),a1))), % 123.67/123.68 inference(scs_inference,[],[11,318,3,21,17])). % 123.67/123.68 cnf(487,plain, % 123.67/123.68 (~P8(f15(x4871,f15(x4872,x4873,f15(x4874,x4875,f8(f15(a1,f10(a1,a3),f9(a3)),a7))),x4876))), % 123.67/123.68 inference(scs_inference,[],[184,23,22])). % 123.67/123.68 cnf(522,plain, % 123.67/123.68 (~P8(f10(x5221,f15(x5222,f15(f8(f14(a2,a3,a7,x5223),a4),x5224,f15(a1,f10(a1,a3),f9(a3))),x5225)))), % 123.67/123.68 inference(scs_inference,[],[326,23,14])). % 123.67/123.68 cnf(523,plain, % 123.67/123.68 (~P8(f15(x5231,f15(f8(f14(a2,a3,a7,x5232),a4),x5233,f15(a1,f10(a1,a3),f9(a3))),x5234))), % 123.67/123.68 inference(scs_inference,[],[35,522,12])). % 123.67/123.68 cnf(526,plain, % 123.67/123.68 (~P8(f15(x5261,f15(x5262,x5263,f15(f8(f14(a2,a3,a7,x5264),a4),x5265,f15(a1,f10(a1,a3),f9(a3)))),x5266))), % 123.67/123.68 inference(scs_inference,[],[326,23,22])). % 123.67/123.68 cnf(527,plain, % 123.67/123.68 (~P8(f15(x5271,x5272,f15(f8(f14(a2,a3,a7,x5273),a4),x5274,f15(a1,f10(a1,a3),f9(a3)))))), % 123.67/123.68 inference(scs_inference,[],[35,526,20])). % 123.67/123.68 cnf(623,plain, % 123.67/123.68 (~P8(f10(f15(f15(f8(f15(a1,f10(a1,a3),f9(a3)),a7),x6231,x6232),x6233,x6234),x6235))), % 123.67/123.68 inference(scs_inference,[],[189,24,15])). % 123.67/123.68 cnf(669,plain, % 123.67/123.68 (~P5(f11(f8(f10(a1,a3),a1),a1))), % 123.67/123.68 inference(scs_inference,[],[416,2,16,13])). % 123.67/123.68 cnf(694,plain, % 123.67/123.68 (~P8(f14(x6941,x6942,x6943,f14(x6944,f15(x6945,x6946,f15(f8(f14(a2,a3,a7,x6947),a4),x6948,f15(a1,f10(a1,a3),f9(a3)))),x6949,x69410)))), % 123.67/123.68 inference(scs_inference,[],[527,27,29])). % 123.67/123.68 cnf(713,plain, % 123.67/123.68 (~P8(f14(x7131,x7132,f14(x7133,f14(x7134,x7135,x7136,f8(f15(a1,f10(a1,a3),f9(a3)),a7)),x7137,x7138),x7139))), % 123.67/123.68 inference(scs_inference,[],[103,27,47])). % 123.67/123.68 cnf(726,plain, % 123.67/123.68 (~P8(f14(x7261,x7262,x7263,f14(x7264,x7265,f14(x7266,f8(f15(a1,f10(a1,a3),f9(a3)),a7),x7267,x7268),x7269)))), % 123.67/123.68 inference(scs_inference,[],[103,27,47])). % 123.67/123.68 cnf(732,plain, % 123.67/123.68 (~P8(f14(x7321,f14(x7322,x7323,f8(f15(a1,f10(a1,a3),f9(a3)),a7),x7324),x7325,x7326))), % 123.67/123.68 inference(scs_inference,[],[103,28,29])). % 123.67/123.68 cnf(738,plain, % 123.67/123.68 (~P8(f14(x7381,x7382,f14(x7383,f14(x7384,x7385,f8(f15(a1,f10(a1,a3),f9(a3)),a7),x7386),x7387,x7388),x7389))), % 123.67/123.68 inference(scs_inference,[],[103,28,47])). % 123.67/123.68 cnf(742,plain, % 123.67/123.68 (~P8(f14(f14(x7421,x7422,f8(f15(a1,f10(a1,a3),f9(a3)),a7),x7423),x7424,x7425,x7426))), % 123.67/123.68 inference(scs_inference,[],[103,28,30])). % 123.67/123.68 cnf(794,plain, % 123.67/123.68 (~P8(f14(x7941,f14(x7942,x7943,f14(x7944,f8(f15(a1,f10(a1,a3),f9(a3)),a7),x7945,x7946),x7947),x7948,x7949))), % 123.67/123.68 inference(scs_inference,[],[103,29,47])). % 123.67/123.68 cnf(831,plain, % 123.67/123.68 (~P8(f14(x8311,x8312,f14(x8313,f14(f8(f15(a1,f10(a1,a3),f9(a3)),a7),x8314,x8315,x8316),x8317,x8318),x8319))), % 123.67/123.68 inference(scs_inference,[],[103,30,47])). % 123.67/123.68 cnf(1099,plain, % 123.67/123.68 (~P8(f15(x10991,f10(f10(f8(f15(a1,f10(a1,a3),f9(a3)),a7),x10992),x10993),x10994))), % 123.67/123.68 inference(scs_inference,[],[116,523,48,44])). % 123.67/123.68 cnf(1150,plain, % 123.67/123.68 (P7(f13(a5,a1,f15(f8(f14(a2,a3,f12(a3),f9(a3)),a4),f8(f15(a1,f12(a3),f9(a3)),a7),f6(a3))))), % 123.67/123.68 inference(scs_inference,[],[1,39,713,321,94,5,2,9,10,27,28,29,30,22,23,14,24,15,21,13,12,17,19,20,34])). % 123.67/123.68 cnf(1156,plain, % 123.67/123.68 (~P7(f13(a1,a2,f10(f8(f15(a1,a3,f9(a3)),a7),f8(f6(a3),a3))))), % 123.67/123.68 inference(scs_inference,[],[1,39,713,321,94,5,2,9,10,27,28,29,30,22,23,14,24,15,21,13,12,17,19,20,34,26,16,46])). % 123.67/123.68 cnf(1158,plain, % 123.67/123.68 (~P7(f13(a1,a2,f10(f8(f15(a1,f8(f10(a1,a3),a1),f9(a3)),a7),f8(f6(a3),f8(f10(a1,a3),a1)))))), % 123.67/123.68 inference(scs_inference,[],[1,39,669,713,321,37,94,5,2,9,10,27,28,29,30,22,23,14,24,15,21,13,12,17,19,20,34,26,16,46,32])). % 123.67/123.68 cnf(1185,plain, % 123.67/123.68 (P9(f11(f8(a3,a3),a1))), % 123.67/123.68 inference(scs_inference,[],[1,231,1156,726,738,8,29,27,28,30,23,22,14,15,24,21,33,13])). % 123.67/123.68 cnf(1233,plain, % 123.67/123.68 (~P7(f13(a1,a2,f10(f8(f15(a1,a2,f9(a3)),a7),f8(f6(a3),a2))))), % 123.67/123.68 inference(scs_inference,[],[1,101,322,1185,794,831,2,29,28,27,30,22,23,14,24,15,21,13,12,17,19,20,26,16,46])). % 123.67/123.68 cnf(5694,plain, % 123.67/123.68 (P7(f13(a1,a2,f10(f8(f15(a1,f12(a3),f9(a3)),a7),f8(f6(a3),f12(a3)))))), % 123.67/123.68 inference(scs_inference,[],[35,8,742,223,732,144,1150,47,43,45,44,21,23,12,33])). % 123.67/123.68 cnf(5698,plain, % 123.67/123.68 (~P8(f10(f8(f15(a1,a3,f9(a3)),a7),f8(f6(a3),a3)))), % 123.67/123.68 inference(scs_inference,[],[1,2,35,8,742,223,732,144,37,1156,1150,47,43,45,44,21,23,12,33,32,19])). % 123.67/123.68 cnf(5710,plain, % 123.67/123.68 (~P8(f14(f15(x57101,x57102,f10(x57103,f10(f8(f15(a1,a3,f9(a3)),a7),f8(f6(a3),a3)))),x57104,x57105,x57106))), % 123.67/123.68 inference(scs_inference,[],[1,2,35,8,742,223,487,732,144,37,1156,694,1150,47,43,45,44,21,23,12,33,32,19,20,26,24,16,48])). % 123.67/123.68 cnf(5712,plain, % 123.67/123.68 (~P8(f12(a3))), % 123.67/123.68 inference(scs_inference,[],[1,2,35,8,742,223,487,732,144,37,1156,694,1150,47,43,45,44,21,23,12,33,32,19,20,26,24,16,48,13])). % 123.67/123.68 cnf(5738,plain, % 123.67/123.68 (~P8(f10(f8(f15(a1,a2,f9(a3)),a7),f8(f6(a3),a2)))), % 123.67/123.68 inference(scs_inference,[],[1,35,2,732,623,144,149,1233,5712,5694,47,43,45,44,21,48,12,19])). % 123.67/123.68 cnf(5743,plain, % 123.67/123.68 (~P8(f15(x57431,x57432,f10(x57433,f10(f8(f15(a1,a3,f9(a3)),a7),f8(f6(a3),a3)))))), % 123.67/123.68 inference(scs_inference,[],[1,35,2,732,623,1099,144,149,1233,5712,5710,5694,47,43,45,44,21,48,12,19,20,26])). % 123.67/123.68 cnf(5766,plain, % 123.67/123.68 ($false), % 123.67/123.68 inference(scs_inference,[],[1,35,2,149,105,188,99,97,214,1158,5698,5738,5743,47,43,45,44,48,12,19,20,17]), % 123.67/123.68 ['proof']). % 123.67/123.68 % SZS output end Proof % 123.67/123.68 % Total time :122.930000s %------------------------------------------------------------------------------