%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWV233+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n011.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 : Wed Jul 27 13:20:15 EDT 2022 % Result : Timeout 299.91s 300.10s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWV233+1 : TPTP v8.1.0. Released v3.2.0. % 0.11/0.13 % Command : otter-tptp-script %s % 0.12/0.34 % Computer : n011.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 : Wed Jul 27 05:57:10 EDT 2022 % 0.12/0.34 % CPUTime : % 2.05/2.23 ----- Otter 3.3f, August 2004 ----- % 2.05/2.23 The process was started by sandbox on n011.cluster.edu, % 2.05/2.23 Wed Jul 27 05:57:10 2022 % 2.05/2.23 The command was "./otter". The process ID is 25492. % 2.05/2.23 % 2.05/2.23 set(prolog_style_variables). % 2.05/2.23 set(auto). % 2.05/2.23 dependent: set(auto1). % 2.05/2.23 dependent: set(process_input). % 2.05/2.23 dependent: clear(print_kept). % 2.05/2.23 dependent: clear(print_new_demod). % 2.05/2.23 dependent: clear(print_back_demod). % 2.05/2.23 dependent: clear(print_back_sub). % 2.05/2.23 dependent: set(control_memory). % 2.05/2.23 dependent: assign(max_mem, 12000). % 2.05/2.23 dependent: assign(pick_given_ratio, 4). % 2.05/2.23 dependent: assign(stats_level, 1). % 2.05/2.23 dependent: assign(max_seconds, 10800). % 2.05/2.23 clear(print_given). % 2.05/2.23 % 2.05/2.23 formula_list(usable). % 2.05/2.23 all A (A=A). % 2.05/2.23 all E1 E2 (knows(encrypt(E1,E2))&knows(inverse(E2))->knows(E1)). % 2.05/2.23 all E1 E2 (knows(symmetric_encrypt(E1,E2))&knows(E2)->knows(E1)). % 2.05/2.23 all E K (knows(sign(E,inverse(K)))&knows(K)->knows(E)). % 2.05/2.23 all E1 E2 (knows(E1)&knows(E2)->knows(concatenate(E1,E2))&knows(encrypt(E1,E2))&knows(symmetric_encrypt(E1,E2))&knows(decrypt(E1,E2))&knows(symmetric_decrypt(E1,E2))&knows(extract(E1,E2))&knows(sign(E1,E2))). % 2.05/2.23 all E1 E2 (knows(concatenate(E1,E2))->knows(E1)&knows(E2)). % 2.05/2.23 all E (knows(E)->knows(head(E))&knows(tail(E))&knows(hash(E))). % 2.05/2.23 all E K (decrypt(encrypt(E,K),inverse(K))=E). % 2.05/2.23 all E K (symmetric_decrypt(symmetric_encrypt(E,K),K)=E). % 2.05/2.23 all E K (extract(sign(E,inverse(K)),K)=E). % 2.05/2.23 all X Y (head(concatenate(X,Y))=X). % 2.05/2.23 all X Y (tail(concatenate(X,Y))=Y). % 2.05/2.23 all X (first(X)=head(X)). % 2.05/2.23 all X (second(X)=head(tail(X))). % 2.05/2.23 all X (third(X)=head(tail(tail(X)))). % 2.05/2.23 all X (fourth(X)=head(tail(tail(tail(X))))). % 2.05/2.23 all X Y (knows(X)&knows(Y)->knows(mac(X,Y))). % 2.05/2.23 knows(k_ca). % 2.05/2.23 knows(inverse(k_a)). % 2.05/2.23 knows(k_a). % 2.05/2.23 all Init_1 Init_2 Init_3 Resp_1 Resp_2 (knows(concatenate(n,concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c)))))& (knows(Resp_1)&knows(Resp_2)&first(extract(Resp_2,k_ca))=s&second(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca))))=n->knows(symmetric_encrypt(secret,first(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca)))))))& (knows(Init_1)&knows(Init_2)&knows(Init_3)&second(extract(Init_3,Init_2))=Init_2->knows(concatenate(encrypt(sign(concatenate(kgen(Init_2),concatenate(Init_1,eol)),inverse(k_s)),Init_2),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca)))))). % 2.05/2.23 -knows(secret). % 2.05/2.23 end_of_list. % 2.05/2.23 % 2.05/2.23 -------> usable clausifies to: % 2.05/2.23 % 2.05/2.23 list(usable). % 2.05/2.23 0 [] A=A. % 2.05/2.23 0 [] -knows(encrypt(E1,E2))| -knows(inverse(E2))|knows(E1). % 2.05/2.23 0 [] -knows(symmetric_encrypt(E1,E2))| -knows(E2)|knows(E1). % 2.05/2.23 0 [] -knows(sign(E,inverse(K)))| -knows(K)|knows(E). % 2.05/2.23 0 [] -knows(E1)| -knows(E2)|knows(concatenate(E1,E2)). % 2.05/2.23 0 [] -knows(E1)| -knows(E2)|knows(encrypt(E1,E2)). % 2.05/2.23 0 [] -knows(E1)| -knows(E2)|knows(symmetric_encrypt(E1,E2)). % 2.05/2.23 0 [] -knows(E1)| -knows(E2)|knows(decrypt(E1,E2)). % 2.05/2.23 0 [] -knows(E1)| -knows(E2)|knows(symmetric_decrypt(E1,E2)). % 2.05/2.23 0 [] -knows(E1)| -knows(E2)|knows(extract(E1,E2)). % 2.05/2.23 0 [] -knows(E1)| -knows(E2)|knows(sign(E1,E2)). % 2.05/2.23 0 [] -knows(concatenate(E1,E2))|knows(E1). % 2.05/2.23 0 [] -knows(concatenate(E1,E2))|knows(E2). % 2.05/2.23 0 [] -knows(E)|knows(head(E)). % 2.05/2.23 0 [] -knows(E)|knows(tail(E)). % 2.05/2.23 0 [] -knows(E)|knows(hash(E)). % 2.05/2.23 0 [] decrypt(encrypt(E,K),inverse(K))=E. % 2.05/2.23 0 [] symmetric_decrypt(symmetric_encrypt(E,K),K)=E. % 2.05/2.23 0 [] extract(sign(E,inverse(K)),K)=E. % 2.05/2.23 0 [] head(concatenate(X,Y))=X. % 2.05/2.23 0 [] tail(concatenate(X,Y))=Y. % 2.05/2.23 0 [] first(X)=head(X). % 2.05/2.23 0 [] second(X)=head(tail(X)). % 2.05/2.23 0 [] third(X)=head(tail(tail(X))). % 2.05/2.23 0 [] fourth(X)=head(tail(tail(tail(X)))). % 2.05/2.23 0 [] -knows(X)| -knows(Y)|knows(mac(X,Y)). % 2.05/2.23 0 [] knows(k_ca). % 2.05/2.23 0 [] knows(inverse(k_a)). % 2.05/2.23 0 [] knows(k_a). % 2.05/2.23 0 [] knows(concatenate(n,concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c))))). % 2.05/2.23 0 [] -knows(Resp_1)| -knows(Resp_2)|first(extract(Resp_2,k_ca))!=s|second(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca))))!=n|knows(symmetric_encrypt(secret,first(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca)))))). % 2.05/2.23 0 [] -knows(Init_1)| -knows(Init_2)| -knows(Init_3)|second(extract(Init_3,Init_2))!=Init_2|knows(concatenate(encrypt(sign(concatenate(kgen(Init_2),concatenate(Init_1,eol)),inverse(k_s)),Init_2),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca)))). % 2.05/2.23 0 [] -knows(secret). % 2.05/2.23 end_of_list. % 2.05/2.23 % 2.05/2.23 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=5. % 2.05/2.23 % 2.05/2.23 This is a Horn set with equality. The strategy will be % 2.05/2.23 Knuth-Bendix and hyper_res, with positive clauses in % 2.05/2.23 sos and nonpositive clauses in usable. % 2.05/2.23 % 2.05/2.23 dependent: set(knuth_bendix). % 2.05/2.23 dependent: set(anl_eq). % 2.05/2.23 dependent: set(para_from). % 2.05/2.23 dependent: set(para_into). % 2.05/2.23 dependent: clear(para_from_right). % 2.05/2.23 dependent: clear(para_into_right). % 2.05/2.23 dependent: set(para_from_vars). % 2.05/2.23 dependent: set(eq_units_both_ways). % 2.05/2.23 dependent: set(dynamic_demod_all). % 2.05/2.23 dependent: set(dynamic_demod). % 2.05/2.23 dependent: set(order_eq). % 2.05/2.23 dependent: set(back_demod). % 2.05/2.23 dependent: set(lrpo). % 2.05/2.23 dependent: set(hyper_res). % 2.05/2.23 dependent: clear(order_hyper). % 2.05/2.23 % 2.05/2.23 ------------> process usable: % 2.05/2.23 ** KEPT (pick-wt=9): 1 [] -knows(encrypt(A,B))| -knows(inverse(B))|knows(A). % 2.05/2.23 ** KEPT (pick-wt=8): 2 [] -knows(symmetric_encrypt(A,B))| -knows(B)|knows(A). % 2.05/2.23 ** KEPT (pick-wt=9): 3 [] -knows(sign(A,inverse(B)))| -knows(B)|knows(A). % 2.05/2.23 ** KEPT (pick-wt=8): 4 [] -knows(A)| -knows(B)|knows(concatenate(A,B)). % 2.05/2.23 ** KEPT (pick-wt=8): 5 [] -knows(A)| -knows(B)|knows(encrypt(A,B)). % 2.05/2.23 ** KEPT (pick-wt=8): 6 [] -knows(A)| -knows(B)|knows(symmetric_encrypt(A,B)). % 2.05/2.23 ** KEPT (pick-wt=8): 7 [] -knows(A)| -knows(B)|knows(decrypt(A,B)). % 2.05/2.23 ** KEPT (pick-wt=8): 8 [] -knows(A)| -knows(B)|knows(symmetric_decrypt(A,B)). % 2.05/2.23 ** KEPT (pick-wt=8): 9 [] -knows(A)| -knows(B)|knows(extract(A,B)). % 2.05/2.23 ** KEPT (pick-wt=8): 10 [] -knows(A)| -knows(B)|knows(sign(A,B)). % 2.05/2.23 ** KEPT (pick-wt=6): 11 [] -knows(concatenate(A,B))|knows(A). % 2.05/2.23 ** KEPT (pick-wt=6): 12 [] -knows(concatenate(A,B))|knows(B). % 2.05/2.23 ** KEPT (pick-wt=5): 13 [] -knows(A)|knows(head(A)). % 2.05/2.23 ** KEPT (pick-wt=5): 14 [] -knows(A)|knows(tail(A)). % 2.05/2.23 ** KEPT (pick-wt=5): 15 [] -knows(A)|knows(hash(A)). % 2.05/2.23 ** KEPT (pick-wt=8): 16 [] -knows(A)| -knows(B)|knows(mac(A,B)). % 2.05/2.23 ** KEPT (pick-wt=35): 17 [] -knows(A)| -knows(B)|first(extract(B,k_ca))!=s|second(extract(decrypt(A,inverse(k_c)),second(extract(B,k_ca))))!=n|knows(symmetric_encrypt(secret,first(extract(decrypt(A,inverse(k_c)),second(extract(B,k_ca)))))). % 2.05/2.23 ** KEPT (pick-wt=33): 18 [] -knows(A)| -knows(B)| -knows(C)|second(extract(C,B))!=B|knows(concatenate(encrypt(sign(concatenate(kgen(B),concatenate(A,eol)),inverse(k_s)),B),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca)))). % 2.05/2.23 ** KEPT (pick-wt=2): 19 [] -knows(secret). % 2.05/2.23 % 2.05/2.23 ------------> process sos: % 2.05/2.23 ** KEPT (pick-wt=3): 20 [] A=A. % 2.05/2.23 ** KEPT (pick-wt=8): 21 [] decrypt(encrypt(A,B),inverse(B))=A. % 2.05/2.23 ---> New Demodulator: 22 [new_demod,21] decrypt(encrypt(A,B),inverse(B))=A. % 2.05/2.23 ** KEPT (pick-wt=7): 23 [] symmetric_decrypt(symmetric_encrypt(A,B),B)=A. % 2.05/2.23 ---> New Demodulator: 24 [new_demod,23] symmetric_decrypt(symmetric_encrypt(A,B),B)=A. % 2.05/2.23 ** KEPT (pick-wt=8): 25 [] extract(sign(A,inverse(B)),B)=A. % 2.05/2.23 ---> New Demodulator: 26 [new_demod,25] extract(sign(A,inverse(B)),B)=A. % 2.05/2.23 ** KEPT (pick-wt=6): 27 [] head(concatenate(A,B))=A. % 2.05/2.23 ---> New Demodulator: 28 [new_demod,27] head(concatenate(A,B))=A. % 2.05/2.23 ** KEPT (pick-wt=6): 29 [] tail(concatenate(A,B))=B. % 2.05/2.23 ---> New Demodulator: 30 [new_demod,29] tail(concatenate(A,B))=B. % 2.05/2.23 ** KEPT (pick-wt=5): 32 [copy,31,flip.1] head(A)=first(A). % 2.05/2.23 ---> New Demodulator: 33 [new_demod,32] head(A)=first(A). % 2.05/2.23 ** KEPT (pick-wt=6): 35 [copy,34,demod,33,flip.1] first(tail(A))=second(A). % 2.05/2.23 ---> New Demodulator: 36 [new_demod,35] first(tail(A))=second(A). % 2.05/2.23 ** KEPT (pick-wt=6): 38 [copy,37,demod,33,36] third(A)=second(tail(A)). % 2.05/2.23 ---> New Demodulator: 39 [new_demod,38] third(A)=second(tail(A)). % 2.05/2.23 ** KEPT (pick-wt=7): 41 [copy,40,demod,33,36,flip.1] second(tail(tail(A)))=fourth(A). % 2.05/2.23 ---> New Demodulator: 42 [new_demod,41] second(tail(tail(A)))=fourth(A). % 2.05/2.23 ** KEPT (pick-wt=2): 43 [] knows(k_ca). % 2.05/2.23 ** KEPT (pick-wt=3): 44 [] knows(inverse(k_a)). % 2.05/2.23 ** KEPT (pick-wt=2): 45 [] knows(k_a). % 2.05/2.23 ** KEPT (pick-wt=13): 46 [] knows(concatenate(n,concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c))))). % 2.05/2.23 Following clause subsumed by 20 during input processing: 0 [copy,20,flip.1] A=A. % 2.05/2.23 >>>> Starting back demodulation with 22. % 2.05/2.23 >>>> Starting back demodulation with 24. % 2.05/2.23 >>>> StartAlarm clock % 299.91/300.10 Otter interrupted % 299.91/300.10 PROOF NOT FOUND %------------------------------------------------------------------------------