%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX065+1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n032.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 : Tue Apr 1 02:15:23 AM UTC 2025 % Result : Unknown 2.95s 3.18s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SWX065+1 : TPTP v9.1.0. Released v9.1.0. % 0.06/0.11 % Command : otter-tptp-script %s % 0.11/0.31 % Computer : n032.cluster.edu % 0.11/0.31 % Model : x86_64 x86_64 % 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.31 % Memory : 8042.1875MB % 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.31 % CPULimit : 300 % 0.11/0.31 % WCLimit : 300 % 0.11/0.31 % DateTime : Mon Mar 31 15:38:16 EDT 2025 % 0.11/0.31 % CPUTime : % 2.95/3.16 ----- Otter 3.3f, August 2004 ----- % 2.95/3.16 The process was started by sandbox on n032.cluster.edu, % 2.95/3.16 Mon Mar 31 15:38:16 2025 % 2.95/3.16 The command was "./otter". The process ID is 14495. % 2.95/3.16 % 2.95/3.16 set(prolog_style_variables). % 2.95/3.16 set(auto). % 2.95/3.16 dependent: set(auto1). % 2.95/3.16 dependent: set(process_input). % 2.95/3.16 dependent: clear(print_kept). % 2.95/3.16 dependent: clear(print_new_demod). % 2.95/3.16 dependent: clear(print_back_demod). % 2.95/3.16 dependent: clear(print_back_sub). % 2.95/3.16 dependent: set(control_memory). % 2.95/3.16 dependent: assign(max_mem, 12000). % 2.95/3.16 dependent: assign(pick_given_ratio, 4). % 2.95/3.16 dependent: assign(stats_level, 1). % 2.95/3.16 dependent: assign(max_seconds, 10800). % 2.95/3.16 clear(print_given). % 2.95/3.16 % 2.95/3.16 formula_list(usable). % 2.95/3.16 % 2.95/3.16 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.16 could not be combined into a single term with special operators. % 2.95/3.16 ' % 2.95/3.16 1 % 2.95/3.16 ' % 2.95/3.16 % 2.95/3.16 The context of the bad sequence is: % 2.95/3.16 % 2.95/3.16 % 2.95/3.16 - ( =(nil, ***HERE*** '1') ). % 2.95/3.16 % 2.95/3.16 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.16 could not be combined into a single term with special operators. % 2.95/3.16 ' % 2.95/3.16 0 % 2.95/3.16 ' % 2.95/3.16 % 2.95/3.16 The context of the bad sequence is: % 2.95/3.16 % 2.95/3.16 % 2.95/3.16 - ( =(nil, ***HERE*** '0') ). % 2.95/3.16 % 2.95/3.16 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.16 could not be combined into a single term with special operators. % 2.95/3.16 ' % 2.95/3.16 1 % 2.95/3.16 ' % 2.95/3.16 % 2.95/3.16 The context of the bad sequence is: % 2.95/3.16 % 2.95/3.16 % 2.95/3.16 ( all Xx20 Xx21 ( - ( =( ***HERE*** '1',cons(Xx20,Xx21)) ) ) ). % 2.95/3.16 % 2.95/3.16 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.16 could not be combined into a single term with special operators. % 2.95/3.16 ' % 2.95/3.16 0 % 2.95/3.16 ' % 2.95/3.16 % 2.95/3.16 The context of the bad sequence is: % 2.95/3.16 % 2.95/3.16 % 2.95/3.16 ( all Xx22 Xx23 ( - ( =( ***HERE*** '0',cons(Xx22,Xx23)) ) ) ). % 2.95/3.16 % 2.95/3.16 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.16 could not be combined into a single term with special operators. % 2.95/3.16 ' % 2.95/3.16 1 % 2.95/3.16 ' % 2.95/3.16 % 2.95/3.16 The context of the bad sequence is: % 2.95/3.16 % 2.95/3.16 % 2.95/3.16 - ( =( ***HERE*** '1','0') ). % 2.95/3.16 % 2.95/3.16 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.16 could not be combined into a single term with special operators. % 2.95/3.16 ' % 2.95/3.16 1 % 2.95/3.16 ' % 2.95/3.16 % 2.95/3.16 The context of the bad sequence is: % 2.95/3.16 % 2.95/3.16 % 2.95/3.16 ( all Xx38 ( - ( =( ***HERE*** '1',p(Xx38)) ) ) ). % 2.95/3.16 % 2.95/3.16 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.16 could not be combined into a single term with special operators. % 2.95/3.16 ' % 2.95/3.16 1 % 2.95/3.16 ' % 2.95/3.16 % 2.95/3.16 The context of the bad sequence is: % 2.95/3.16 % 2.95/3.16 % 2.95/3.16 ( all Xx39 ( - ( =( ***HERE*** '1',neg(Xx39)) ) ) ). % 2.95/3.16 % 2.95/3.16 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.16 could not be combined into a single term with special operators. % 2.95/3.16 ' % 2.95/3.16 1 % 2.95/3.16 ' % 2.95/3.16 % 2.95/3.16 The context of the bad sequence is: % 2.95/3.16 % 2.95/3.16 % 2.95/3.16 ( all Xx40 Xx41 ( - ( =( ***HERE*** '1',and(Xx40,Xx41)) ) ) ). % 2.95/3.16 % 2.95/3.16 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.16 could not be combined into a single term with special operators. % 2.95/3.16 ' % 2.95/3.16 1 % 2.95/3.16 ' % 2.95/3.16 % 2.95/3.16 The context of the bad sequence is: % 2.95/3.16 % 2.95/3.16 % 2.95/3.16 ( all Xx42 Xx43 ( - ( =( ***HERE*** '1',or(Xx42,Xx43)) ) ) ). % 2.95/3.16 % 2.95/3.16 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.16 could not be combined into a single term with special operators. % 2.95/3.16 ' % 2.95/3.16 0 % 2.95/3.16 ' % 2.95/3.16 % 2.95/3.16 The context of the bad sequence is: % 2.95/3.16 % 2.95/3.16 % 2.95/3.16 ( all Xx44 ( - ( =( ***HERE*** '0',p(Xx44)) ) ) ). % 2.95/3.16 % 2.95/3.16 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.16 could not be combined into a single term with special operators. % 2.95/3.16 ' % 2.95/3.16 0 % 2.95/3.16 ' % 2.95/3.16 % 2.95/3.16 The context of the bad sequence is: % 2.95/3.16 % 2.95/3.16 % 2.95/3.16 ( all Xx45 ( - ( =( ***HERE*** '0',neg(Xx45)) ) ) ). % 2.95/3.16 % 2.95/3.16 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.16 could not be combined into a single term with special operators. % 2.95/3.16 ' % 2.95/3.16 0 % 2.95/3.16 ' % 2.95/3.16 % 2.95/3.16 The context of the bad sequence is: % 2.95/3.16 % 2.95/3.16 % 2.95/3.16 ( all Xx46 Xx47 ( - ( =( ***HERE*** '0',and(Xx46,Xx47)) ) ) ). % 2.95/3.16 % 2.95/3.16 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.16 could not be combined into a single term with special operators. % 2.95/3.16 ' % 2.95/3.16 0 % 2.95/3.16 ' % 2.95/3.16 % 2.95/3.16 The context of the bad sequence is: % 2.95/3.16 % 2.95/3.16 % 2.95/3.16 ( all Xx48 Xx49 ( - ( =( ***HERE*** '0',or(Xx48,Xx49)) ) ) ). % 2.95/3.16 % 2.95/3.16 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.16 could not be combined into a single term with special operators. % 2.95/3.16 ' % 2.95/3.16 1 % 2.95/3.16 ' % 2.95/3.16 % 2.95/3.16 The context of the bad sequence is: % 2.95/3.16 % 2.95/3.16 % 2.95/3.16 gr( ***HERE*** '1'). % 2.95/3.16 % 2.95/3.16 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.16 could not be combined into a single term with special operators. % 2.95/3.18 ' % 2.95/3.18 0 % 2.95/3.18 ' % 2.95/3.18 % 2.95/3.18 The context of the bad sequence is: % 2.95/3.18 % 2.95/3.18 % 2.95/3.18 gr( ***HERE*** '0'). % 2.95/3.18 % 2.95/3.18 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.18 could not be combined into a single term with special operators. % 2.95/3.18 ' % 2.95/3.18 0 % 2.95/3.18 ' % 2.95/3.18 % 2.95/3.18 The context of the bad sequence is: % 2.95/3.18 % 2.95/3.18 % 2.95/3.18 ( all Xx1 Xx2 Xx3 ( % 2.95/3.18 ( eval_succeeds(Xx1,Xx2,Xx3) % 2.95/3.18 <-> ( ( exists Xx4 Xx5 ( % 2.95/3.18 ( =(Xx1,or(Xx4,Xx5)) % 2.95/3.18 & =(Xx3, ***HERE*** '0') % 2.95/3.18 & eval_succeeds(Xx4,Xx2,'0') % 2.95/3.18 & eval_succeeds(Xx5,Xx2,'0') ) ) ) % 2.95/3.18 | ( exists Xx6 Xx7 ( % 2.95/3.18 ( =(Xx1,or(Xx6,Xx7)) % 2.95/3.18 & =(Xx3,'1') % 2.95/3.18 & eval_succeeds(Xx7,Xx2,'1') ) ) ) % 2.95/3.18 | ( exists Xx8 Xx9 ( % 2.95/3.18 ( =(Xx1,or(Xx8,Xx9)) % 2.95/3.18 & =(Xx3,'1') % 2.95/3.18 & eval_succeeds(Xx8,Xx2,'1') ) ) ) % 2.95/3.18 | ( exists Xx10 Xx11 ( % 2.95/3.18 ( =(Xx1,and(Xx10,Xx11)) % 2.95/3.18 & =(Xx3,'0') % 2.95/3.18 & eval_succeeds(Xx11,Xx2,'0') ) ) ) % 2.95/3.18 | ( exists Xx12 Xx13 ( % 2.95/3.18 ( =(Xx1,and(Xx12,Xx13)) % 2.95/3.18 & =(Xx3,'0') % 2.95/3.18 & eval_succeeds(Xx12,Xx2,'0') ) ) ) % 2.95/3.18 | ( exists Xx14 Xx15 ( % 2.95/3.18 ( =(Xx1,and(Xx14,Xx15)) % 2.95/3.18 & =(Xx3,'1') % 2.95/3.18 & eval_succeeds(Xx14,Xx2,'1') % 2.95/3.18 & eval_succeeds(Xx15,Xx2,'1') ) ) ) % 2.95/3.18 | ( exists Xx16 ( % 2.95/3.18 ( =(Xx1,neg(Xx16)) % 2.95/3.18 & =(Xx3,'0') % 2.95/3.18 & eval_succeeds(Xx16,Xx2,'1') ) ) ) % 2.95/3.18 | ( exists Xx17 ( % 2.95/3.18 ( =(Xx1,neg(Xx17)) % 2.95/3.18 & =(Xx3,'1') % 2.95/3.18 & eval_succeeds(Xx17,Xx2,'0') ) ) ) % 2.95/3.18 | ( exists Xx18 ( % 2.95/3.18 ( =(Xx1,p(Xx18)) % 2.95/3.18 & =(Xx3,'0') % 2.95/3.18 & member_succeeds(neg(p(Xx18)),Xx2) ) ) ) % 2.95/3.18 | ( exists Xx19 ( % 2.95/3.18 ( =(Xx1,p(Xx19)) % 2.95/3.18 & =(Xx3,'1') % 2.95/3.18 & member_succeeds(p(Xx19),Xx2) ) ) ) ) ) ) ). % 2.95/3.18 % 2.95/3.18 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.18 could not be combined into a single term with special operators. % 2.95/3.18 ' % 2.95/3.18 0 % 2.95/3.18 ' % 2.95/3.18 % 2.95/3.18 The context of the bad sequence is: % 2.95/3.18 % 2.95/3.18 % 2.95/3.18 ( all Xx1 Xx2 Xx3 ( % 2.95/3.18 ( eval_fails(Xx1,Xx2,Xx3) % 2.95/3.18 <-> ( ( all Xx4 Xx5 ( % 2.95/3.18 ( - ( =(Xx1,or(Xx4,Xx5)) ) % 2.95/3.18 | - ( =(Xx3, ***HERE*** '0') ) % 2.95/3.18 | eval_fails(Xx4,Xx2,'0') % 2.95/3.18 | eval_fails(Xx5,Xx2,'0') ) ) ) % 2.95/3.18 & ( all Xx6 Xx7 ( % 2.95/3.18 ( - ( =(Xx1,or(Xx6,Xx7)) ) % 2.95/3.18 | - ( =(Xx3,'1') ) % 2.95/3.18 | eval_fails(Xx7,Xx2,'1') ) ) ) % 2.95/3.18 & ( all Xx8 Xx9 ( % 2.95/3.18 ( - ( =(Xx1,or(Xx8,Xx9)) ) % 2.95/3.18 | - ( =(Xx3,'1') ) % 2.95/3.18 | eval_fails(Xx8,Xx2,'1') ) ) ) % 2.95/3.18 & ( all Xx10 Xx11 ( % 2.95/3.18 ( - ( =(Xx1,and(Xx10,Xx11)) ) % 2.95/3.18 | - ( =(Xx3,'0') ) % 2.95/3.18 | eval_fails(Xx11,Xx2,'0') ) ) ) % 2.95/3.18 & ( all Xx12 Xx13 ( % 2.95/3.18 ( - ( =(Xx1,and(Xx12,Xx13)) ) % 2.95/3.18 | - ( =(Xx3,'0') ) % 2.95/3.18 | eval_fails(Xx12,Xx2,'0') ) ) ) % 2.95/3.18 & ( all Xx14 Xx15 ( % 2.95/3.18 ( - ( =(Xx1,and(Xx14,Xx15)) ) % 2.95/3.18 | - ( =(Xx3,'1') ) % 2.95/3.18 | eval_fails(Xx14,Xx2,'1') % 2.95/3.18 | eval_fails(Xx15,Xx2,'1') ) ) ) % 2.95/3.18 & ( all Xx16 ( % 2.95/3.18 ( - ( =(Xx1,neg(Xx16)) ) % 2.95/3.18 | - ( =(Xx3,'0') ) % 2.95/3.18 | eval_fails(Xx16,Xx2,'1') ) ) ) % 2.95/3.18 & ( all Xx17 ( % 2.95/3.18 ( - ( =(Xx1,neg(Xx17)) ) % 2.95/3.18 | - ( =(Xx3,'1') ) % 2.95/3.18 | eval_fails(Xx17,Xx2,'0') ) ) ) % 2.95/3.18 & ( all Xx18 ( % 2.95/3.18 ( - ( =(Xx1,p(Xx18)) ) % 2.95/3.18 | - ( =(Xx3,'0') ) % 2.95/3.18 | member_fails(neg(p(Xx18)),Xx2) ) ) ) % 2.95/3.18 & ( all Xx19 ( % 2.95/3.18 ( - ( =(Xx1,p(Xx19)) ) % 2.95/3.18 | - ( =(Xx3,'1') ) % 2.95/3.18 | member_fails(p(Xx19),Xx2) ) ) ) ) ) ) ). % 2.95/3.18 % 2.95/3.18 ERROR, the 3 terms/operators in the following sequence are OK, but they % 2.95/3.18 could not be combined into a single term with special operators. % 2.95/3.18 ' % 2.95/3.18 0 % 2.95/3.18 ' % 2.95/3.18 % 2.95/3.18 The context of the bad sequence is: % 2.95/3.18 % 2.95/3.18 % 2.95/3.18 ( all Xx1 Xx2 Xx3 ( % 2.95/3.18 ( eval_terminates(Xx1,Xx2,Xx3) % 2.95/3.18 <-> ( ( all Xx4 Xx5 ( % 2.95/3.18 ( - ( =(Xx1,or(Xx4,Xx5)) ) % 2.95/3.18 | - ( =(Xx3, ***HERE*** '0') ) % 2.95/3.18 | ( eval_terminates(Xx4,Xx2,'0') % 2.95/3.18 & ( eval_fails(Xx4,Xx2,'0') % 2.95/3.18 | eval_terminates(Xx5,Xx2,'0') ) ) ) ) ) % 2.95/3.18 & ( all Xx6 Xx7 ( % 2.95/3.18 ( - ( =(Xx1,or(Xx6,Xx7)) ) % 2.95/3.18 | - ( =(Xx3,'1') ) % 2.95/3.18 | eval_terminates(Xx7,Xx2,'1') ) ) ) % 2.95/3.18 & ( all Xx8 Xx9 ( % 2.95/3.18 ( - ( =(Xx1,or(Xx8,Xx9)) ) % 2.95/3.18 | - ( =(Xx3,'1') ) % 2.95/3.18 | eval_terminates(Xx8,Xx2,'1') ) ) ) % 2.95/3.18 & ( all Xx10 Xx11 ( % 2.95/3.18 ( - ( =(Xx1,and(Xx10,Xx11)) ) % 2.95/3.18 | - ( =(Xx3,'0') ) % 2.95/3.18 | eval_terminates(Xx11,Xx2,'0') ) ) ) % 2.95/3.18 & ( all Xx12 Xx13 ( % 2.95/3.18 ( - ( =(Xx1,and(Xx12,Xx13)) ) % 2.95/3.18 | - ( =(Xx3,'0') ) % 2.95/3.18 | eval_terminates(Xx12,Xx2,'0') ) ) ) % 2.95/3.18 & ( all Xx14 Xx15 ( % 2.95/3.18 ( - ( =(Xx1,and(Xx14,Xx15)) ) % 2.95/3.18 | - ( =(Xx3,'1') ) % 2.95/3.18 | ( eval_terminates(Xx14,Xx2,'1') % 2.95/3.18 & ( eval_fails(Xx14,Xx2,'1') % 2.95/3.18 | eval_terminates(Xx15,Xx2,'1') ) ) ) ) ) % 2.95/3.18 & ( all Xx16 ( % 2.95/3.18 ( - ( =(Xx1,neg(Xx16)) ) % 2.95/3.18 | - ( =(Xx3,'0') ) % 2.95/3.18 | eval_terminates(Xx16,Xx2,'1') ) ) ) % 2.95/3.18 & ( all Xx17 ( % 2.95/3.18 ( - ( =(Xx1,neg(Xx17)) ) % 2.95/3.18 | - ( =(Xx3,'1') ) % 2.95/3.18 | eval_terminates(Xx17,Xx2,'0') ) ) ) % 2.95/3.18 & ( all Xx18 ( % 2.95/3.18 ( - ( =(Xx1,p(Xx18)) ) % 2.95/3.18 | - ( =(Xx3,'0') ) % 2.95/3.18 | member_terminates(neg(p(Xx18)),Xx2) ) ) ) % 2.95/3.18 & ( all Xx19 ( % 2.95/3.18 ( - ( =(Xx1,p(Xx19)) ) % 2.95/3.18 | - ( =(Xx3,'1') ) % 2.95/3.18 | member_terminates(p(Xx19),Xx2) ) ) ) ) ) ) ). % 2.95/3.18 all A (A=A). % 2.95/3.18 all Xx4 Xx5 (nil!=cons(Xx4,Xx5)). % 2.95/3.18 all Xx6 (nil!=p(Xx6)). % 2.95/3.18 all Xx7 (nil!=neg(Xx7)). % 2.95/3.18 all Xx8 Xx9 (nil!=and(Xx8,Xx9)). % 2.95/3.18 all Xx10 Xx11 (nil!=or(Xx10,Xx11)). % 2.95/3.18 all Xx12 Xx13 Xx14 Xx15 (cons(Xx12,Xx13)=cons(Xx14,Xx15)->Xx13=Xx15). % 2.95/3.18 all Xx16 Xx17 Xx18 Xx19 (cons(Xx16,Xx17)=cons(Xx18,Xx19)->Xx16=Xx18). % 2.95/3.18 all Xx24 Xx25 Xx26 (cons(Xx24,Xx25)!=p(Xx26)). % 2.95/3.18 all Xx27 Xx28 Xx29 (cons(Xx27,Xx28)!=neg(Xx29)). % 2.95/3.18 all Xx30 Xx31 Xx32 Xx33 (cons(Xx30,Xx31)!=and(Xx32,Xx33)). % 2.95/3.18 all Xx34 Xx35 Xx36 Xx37 (cons(Xx34,Xx35)!=or(Xx36,Xx37)). % 2.95/3.18 all Xx50 Xx51 (p(Xx50)=p(Xx51)->Xx50=Xx51). % 2.95/3.18 all Xx52 Xx53 (p(Xx52)!=neg(Xx53)). % 2.95/3.18 all Xx54 Xx55 Xx56 (p(Xx54)!=and(Xx55,Xx56)). % 2.95/3.18 all Xx57 Xx58 Xx59 (p(Xx57)!=or(Xx58,Xx59)). % 2.95/3.18 all Xx60 Xx61 (neg(Xx60)=neg(Xx61)->Xx60=Xx61). % 2.95/3.18 all Xx62 Xx63 Xx64 (neg(Xx62)!=and(Xx63,Xx64)). % 2.95/3.18 all Xx65 Xx66 Xx67 (neg(Xx65)!=or(Xx66,Xx67)). % 2.95/3.18 all Xx68 Xx69 Xx70 Xx71 (and(Xx68,Xx69)=and(Xx70,Xx71)->Xx69=Xx71). % 2.95/3.18 all Xx72 Xx73 Xx74 Xx75 (and(Xx72,Xx73)=and(Xx74,Xx75)->Xx72=Xx74). % 2.95/3.18 all Xx76 Xx77 Xx78 Xx79 (and(Xx76,Xx77)!=or(Xx78,Xx79)). % 2.95/3.18 all Xx80 Xx81 Xx82 Xx83 (or(Xx80,Xx81)=or(Xx82,Xx83)->Xx81=Xx83). % 2.95/3.18 all Xx84 Xx85 Xx86 Xx87 (or(Xx84,Xx85)=or(Xx86,Xx87)->Xx84=Xx86). % 2.95/3.18 gr(nil). % 2.95/3.18 all Xx88 Xx89 (gr(Xx88)&gr(Xx89)<->gr(cons(Xx88,Xx89))). % 2.95/3.18 all Xx90 (gr(Xx90)<->gr(p(Xx90))). % 2.95/3.18 all Xx91 (gr(Xx91)<->gr(neg(Xx91))). % 2.95/3.18 all Xx92 Xx93 (gr(Xx92)&gr(Xx93)<->gr(and(Xx92,Xx93))). % 2.95/3.18 all Xx94 Xx95 (gr(Xx94)&gr(Xx95)<->gr(or(Xx94,Xx95))). % 2.95/3.18 all Xx96 Xx97 (-(defined_succeeds(Xx96,Xx97)&defined_fails(Xx96,Xx97))). % 2.95/3.18 all Xx96 Xx97 (defined_terminates(Xx96,Xx97)->defined_succeeds(Xx96,Xx97)|defined_fails(Xx96,Xx97)). % 2.95/3.18 all Xx98 Xx99 Xx100 (-(eval_succeeds(Xx98,Xx99,Xx100)&eval_fails(Xx98,Xx99,Xx100))). % 2.95/3.18 all Xx98 Xx99 Xx100 (eval_terminates(Xx98,Xx99,Xx100)->eval_succeeds(Xx98,Xx99,Xx100)|eval_fails(Xx98,Xx99,Xx100)). % 2.95/3.18 all Xx101 Xx102 Xx103 (-(false_succeeds(Xx101,Xx102,Xx103)&false_fails(Xx101,Xx102,Xx103))). % 2.95/3.18 all Xx101 Xx102 Xx103 (false_terminates(Xx101,Xx102,Xx103)->false_succeeds(Xx101,Xx102,Xx103)|false_fails(Xx101,Xx102,Xx103)). % 2.95/3.18 all Xx104 Xx105 Xx106 (-(true_succeeds(Xx104,Xx105,Xx106)&true_fails(Xx104,Xx105,Xx106))). % 2.95/3.18 all Xx104 Xx105 Xx106 (true_terminates(Xx104,Xx105,Xx106)->true_succeeds(Xx104,Xx105,Xx106)|true_fails(Xx104,Xx105,Xx106)). % 2.95/3.18 all Xx107 (-(satisfiable_succeeds(Xx107)&satisfiable_fails(Xx107))). % 2.95/3.18 all Xx107 (satisfiable_terminates(Xx107)->satisfiable_succeeds(Xx107)|satisfiable_fails(Xx107)). % 2.95/3.18 all Xx108 (-(valid_succeeds(Xx108)&valid_fails(Xx108))). % 2.95/3.18 all Xx108 (valid_terminates(Xx108)->valid_succeeds(Xx108)|valid_fails(Xx108)). % 2.95/3.18 all Xx109 (-(incon_succeeds(Xx109)&incon_fails(Xx109))). % 2.95/3.18 all Xx109 (incon_terminates(Xx109)->incon_succeeds(Xx109)|incon_fails(Xx109)). % 2.95/3.18 all Xx110 (-(interpretation_succeeds(Xx110)&interpretation_fails(Xx110))). % 2.95/3.18 all Xx110 (interpretation_terminates(Xx110)->interpretation_succeeds(Xx110)|interpretation_fails(Xx110)). % 2.95/3.18 all Xx111 (-(literal_list_succeeds(Xx111)&literal_list_fails(Xx111))). % 2.95/3.18 all Xx111 (literal_list_terminates(Xx111)->literal_list_succeeds(Xx111)|literal_list_fails(Xx111)). % 2.95/3.18 all Xx112 (-(literal_succeeds(Xx112)&literal_fails(Xx112))). % 2.95/3.18 all Xx112 (literal_terminates(Xx112)->literal_succeeds(Xx112)|literal_fails(Xx112)). % 2.95/3.18 all Xx113 (-(formula_succeeds(Xx113)&formula_fails(Xx113))). % 2.95/3.18 all Xx113 (formula_terminates(Xx113)->formula_succeeds(Xx113)|formula_fails(Xx113)). % 2.95/3.18 all Xx114 Xx115 (-(member_succeeds(Xx114,Xx115)&member_fails(Xx114,Xx115))). % 2.95/3.18 all Xx114 Xx115 (member_terminates(Xx114,Xx115)->member_succeeds(Xx114,Xx115)|member_fails(Xx114,Xx115)). % 2.95/3.18 all Xx116 (-(list_succeeds(Xx116)&list_fails(Xx116))). % 2.95/3.18 all Xx116 (list_terminates(Xx116)->list_succeeds(Xx116)|list_fails(Xx116)). % 2.95/3.18 all Xx1 Xx2 (defined_succeeds(Xx1,Xx2)<-> (exists Xx3 Xx4 (Xx1=or(Xx3,Xx4)&defined_succeeds(Xx3,Xx2)&defined_succeeds(Xx4,Xx2)))| (exists Xx5 Xx6 (Xx1=and(Xx5,Xx6)&defined_succeeds(Xx5,Xx2)&defined_succeeds(Xx6,Xx2)))| (exists Xx7 (Xx1=neg(Xx7)&defined_succeeds(Xx7,Xx2)))| (exists Xx8 (Xx1=p(Xx8)&member_succeeds(neg(p(Xx8)),Xx2)))| (exists Xx9 (Xx1=p(Xx9)&member_succeeds(p(Xx9),Xx2)))). % 2.95/3.18 all Xx1 Xx2 (defined_fails(Xx1,Xx2)<-> (all Xx3 Xx4 (Xx1!=or(Xx3,Xx4)|defined_fails(Xx3,Xx2)|defined_fails(Xx4,Xx2)))& (all Xx5 Xx6 (Xx1!=and(Xx5,Xx6)|defined_fails(Xx5,Xx2)|defined_fails(Xx6,Xx2)))& (all Xx7 (Xx1!=neg(Xx7)|defined_fails(Xx7,Xx2)))& (all Xx8 (Xx1!=p(Xx8)|member_fails(neg(p(Xx8)),Xx2)))& (all Xx9 (Xx1!=p(Xx9)|member_fails(p(Xx9),Xx2)))). % 2.95/3.18 all Xx1 Xx2 (defined_terminates(Xx1,Xx2)<-> (all Xx3 Xx4 (Xx1!=or(Xx3,Xx4)|defined_terminates(Xx3,Xx2)& (defined_fails(Xx3,Xx2)|defined_terminates(Xx4,Xx2))))& (all Xx5 Xx6 (Xx1!=and(Xx5,Xx6)|defined_terminates(Xx5,Xx2)& (defined_fails(Xx5,Xx2)|defined_terminates(Xx6,Xx2))))& (all Xx7 (Xx1!=neg(Xx7)|defined_terminates(Xx7,Xx2)))& (all Xx8 (Xx1!=p(Xx8)|member_terminates(neg(p(Xx8)),Xx2)))& (all Xx9 (Xx1!=p(Xx9)|member_terminates(p(Xx9),Xx2)))). % 2.95/3.18 all Xx1 Xx2 Xx3 (false_succeeds(Xx1,Xx2,Xx3)<-> (exists Xx4 Xx5 Xx6 (Xx1=or(Xx4,Xx5)&false_succeeds(Xx4,Xx2,Xx6)&false_succeeds(Xx5,Xx6,Xx3)))| (exists Xx7 Xx8 (Xx1=and(Xx7,Xx8)&false_succeeds(Xx8,Xx2,Xx3)))| (exists Xx9 Xx10 (Xx1=and(Xx9,Xx10)&false_succeeds(Xx9,Xx2,Xx3)))| (exists Xx11 (Xx1=neg(Xx11)&true_succeeds(Xx11,Xx2,Xx3)))| (exists Xx12 (Xx1=p(Xx12)&Xx3=cons(neg(p(Xx12)),Xx2)&member_fails(p(Xx12),Xx2)))). % 2.95/3.18 all Xx1 Xx2 Xx3 (false_fails(Xx1,Xx2,Xx3)<-> (all Xx4 Xx5 Xx6 (Xx1!=or(Xx4,Xx5)|false_fails(Xx4,Xx2,Xx6)|false_fails(Xx5,Xx6,Xx3)))& (all Xx7 Xx8 (Xx1!=and(Xx7,Xx8)|false_fails(Xx8,Xx2,Xx3)))& (all Xx9 Xx10 (Xx1!=and(Xx9,Xx10)|false_fails(Xx9,Xx2,Xx3)))& (all Xx11 (Xx1!=neg(Xx11)|true_fails(Xx11,Xx2,Xx3)))& (all Xx12 (Xx1!=p(Xx12)|Xx3!=cons(neg(p(Xx12)),Xx2)|member_succeeds(p(Xx12),Xx2)))). % 2.95/3.18 all Xx1 Xx2 Xx3 (false_terminates(Xx1,Xx2,Xx3)<-> (all Xx4 Xx5 Xx6 (Xx1!=or(Xx4,Xx5)|false_terminates(Xx4,Xx2,Xx6)& (false_fails(Xx4,Xx2,Xx6)|false_terminates(Xx5,Xx6,Xx3))))& (all Xx7 Xx8 (Xx1!=and(Xx7,Xx8)|false_terminates(Xx8,Xx2,Xx3)))& (all Xx9 Xx10 (Xx1!=and(Xx9,Xx10)|false_terminates(Xx9,Xx2,Xx3)))& (all Xx11 (Xx1!=neg(Xx11)|true_terminates(Xx11,Xx2,Xx3)))& (all Xx12 (Xx1!=p(Xx12)|Xx3!=cons(neg(p(Xx12)),Xx2)|member_terminates(p(Xx12),Xx2)&gr(p(Xx12))&gr(Xx2)))). % 2.95/3.18 all Xx1 Xx2 Xx3 (true_succeeds(Xx1,Xx2,Xx3)<-> (exists Xx4 Xx5 (Xx1=or(Xx4,Xx5)&true_succeeds(Xx5,Xx2,Xx3)))| (exists Xx6 Xx7 (Xx1=or(Xx6,Xx7)&true_succeeds(Xx6,Xx2,Xx3)))| (exists Xx8 Xx9 Xx10 (Xx1=and(Xx8,Xx9)&true_succeeds(Xx8,Xx2,Xx10)&true_succeeds(Xx9,Xx10,Xx3)))| (exists Xx11 (Xx1=neg(Xx11)&false_succeeds(Xx11,Xx2,Xx3)))| (exists Xx12 (Xx1=p(Xx12)&Xx3=cons(p(Xx12),Xx2)&member_fails(neg(p(Xx12)),Xx2)))). % 2.95/3.18 all Xx1 Xx2 Xx3 (true_fails(Xx1,Xx2,Xx3)<-> (all Xx4 Xx5 (Xx1!=or(Xx4,Xx5)|true_fails(Xx5,Xx2,Xx3)))& (all Xx6 Xx7 (Xx1!=or(Xx6,Xx7)|true_fails(Xx6,Xx2,Xx3)))& (all Xx8 Xx9 Xx10 (Xx1!=and(Xx8,Xx9)|true_fails(Xx8,Xx2,Xx10)|true_fails(Xx9,Xx10,Xx3)))& (all Xx11 (Xx1!=neg(Xx11)|false_fails(Xx11,Xx2,Xx3)))& (all Xx12 (Xx1!=p(Xx12)|Xx3!=cons(p(Xx12),Xx2)|member_succeeds(neg(p(Xx12)),Xx2)))). % 2.95/3.18 all Xx1 Xx2 Xx3 (true_terminates(Xx1,Xx2,Xx3)<-> (all Xx4 Xx5 (Xx1!=or(Xx4,Xx5)|true_terminates(Xx5,Xx2,Xx3)))& (all Xx6 Xx7 (Xx1!=or(Xx6,Xx7)|true_terminates(Xx6,Xx2,Xx3)))& (all Xx8 Xx9 Xx10 (Xx1!=and(Xx8,Xx9)|true_terminates(Xx8,Xx2,Xx10)& (true_fails(Xx8,Xx2,Xx10)|true_terminates(Xx9,Xx10,Xx3))))& (all Xx11 (Xx1!=neg(Xx11)|false_terminates(Xx11,Xx2,Xx3)))& (all Xx12 (Xx1!=p(Xx12)|Xx3!=cons(p(Xx12),Xx2)|member_terminates(neg(p(Xx12)),Xx2)&gr(neg(p(Xx12)))&gr(Xx2)))). % 2.95/3.18 all Xx1 (satisfiable_succeeds(Xx1)<-> (exists Xx2 true_succeeds(Xx1,nil,Xx2))). % 2.95/3.18 all Xx1 (satisfiable_fails(Xx1)<-> (all Xx2 true_fails(Xx1,nil,Xx2))). % 2.95/3.18 all Xx1 (satisfiable_terminates(Xx1)<-> (all Xx2 true_terminates(Xx1,nil,Xx2))). % 2.95/3.18 all Xx1 (valid_succeeds(Xx1)<->satisfiable_fails(neg(Xx1))). % 2.95/3.18 all Xx1 (valid_fails(Xx1)<->satisfiable_succeeds(neg(Xx1))). % 2.95/3.18 all Xx1 (valid_terminates(Xx1)<->satisfiable_terminates(neg(Xx1))&gr(neg(Xx1))). % 2.95/3.18 all Xx1 (incon_succeeds(Xx1)<-> (exists Xx2 (member_succeeds(p(Xx2),Xx1)&member_succeeds(neg(p(Xx2)),Xx1)))). % 2.95/3.18 all Xx1 (incon_fails(Xx1)<-> (all Xx2 (member_fails(p(Xx2),Xx1)|member_fails(neg(p(Xx2)),Xx1)))). % 2.95/3.18 all Xx1 (incon_terminates(Xx1)<-> (all Xx2 (member_terminates(p(Xx2),Xx1)& (member_fails(p(Xx2),Xx1)|member_terminates(neg(p(Xx2)),Xx1))))). % 2.95/3.18 all Xx1 (interpretation_succeeds(Xx1)<->literal_list_succeeds(Xx1)&incon_fails(Xx1)). % 2.95/3.18 all Xx1 (interpretation_fails(Xx1)<->literal_list_fails(Xx1)|incon_succeeds(Xx1)). % 2.95/3.18 all Xx1 (interpretation_terminates(Xx1)<->literal_list_terminates(Xx1)& (literal_list_fails(Xx1)|incon_terminates(Xx1)&gr(Xx1))). % 2.95/3.18 all Xx1 (literal_list_succeeds(Xx1)<-> (exists Xx2 Xx3 (Xx1=cons(Xx2,Xx3)&literal_succeeds(Xx2)&literal_list_succeeds(Xx3)))|Xx1=nil). % 2.95/3.18 all Xx1 (literal_list_fails(Xx1)<-> (all Xx2 Xx3 (Xx1!=cons(Xx2,Xx3)|literal_fails(Xx2)|literal_list_fails(Xx3)))&Xx1!=nil). % 2.95/3.18 all Xx1 (literal_list_terminates(Xx1)<-> (all Xx2 Xx3 (Xx1!=cons(Xx2,Xx3)|literal_terminates(Xx2)& (literal_fails(Xx2)|literal_list_terminates(Xx3))))). % 2.95/3.18 all Xx1 (literal_succeeds(Xx1)<-> (exists Xx2 (Xx1=neg(p(Xx2))))| (exists Xx3 (Xx1=p(Xx3)))). % 2.95/3.18 all Xx1 (literal_fails(Xx1)<-> (all Xx2 (Xx1!=neg(p(Xx2))))& (all Xx3 (Xx1!=p(Xx3)))). % 2.95/3.18 all Xx1 (literal_terminates(Xx1)<-> (all Xx2 $T)& (all Xx3 $T)). % 2.95/3.18 all Xx1 (formula_succeeds(Xx1)<-> (exists Xx2 Xx3 (Xx1=or(Xx2,Xx3)&formula_succeeds(Xx2)&formula_succeeds(Xx3)))| (exists Xx4 Xx5 (Xx1=and(Xx4,Xx5)&formula_succeeds(Xx4)&formula_succeeds(Xx5)))| (exists Xx6 (Xx1=neg(Xx6)&formula_succeeds(Xx6)))| (exists Xx7 (Xx1=p(Xx7)))). % 2.95/3.18 all Xx1 (formula_fails(Xx1)<-> (all Xx2 Xx3 (Xx1!=or(Xx2,Xx3)|formula_fails(Xx2)|formula_fails(Xx3)))& (all Xx4 Xx5 (Xx1!=and(Xx4,Xx5)|formula_fails(Xx4)|formula_fails(Xx5)))& (all Xx6 (Xx1!=neg(Xx6)|formula_fails(Xx6)))& (all Xx7 (Xx1!=p(Xx7)))). % 2.95/3.18 all Xx1 (formula_terminates(Xx1)<-> (all Xx2 Xx3 (Xx1!=or(Xx2,Xx3)|formula_terminates(Xx2)& (formula_fails(Xx2)|formula_terminates(Xx3))))& (all Xx4 Xx5 (Xx1!=and(Xx4,Xx5)|formula_terminates(Xx4)& (formula_fails(Xx4)|formula_terminates(Xx5))))& (all Xx6 (Xx1!=neg(Xx6)|formula_terminates(Xx6)))& (all Xx7 $T)). % 2.95/3.18 all Xx1 Xx2 (member_succeeds(Xx1,Xx2)<-> (exists Xx3 Xx4 (Xx2=cons(Xx3,Xx4)&member_succeeds(Xx1,Xx4)))| (exists Xx5 (Xx2=cons(Xx1,Xx5)))). % 2.95/3.18 all Xx1 Xx2 (member_fails(Xx1,Xx2)<-> (all Xx3 Xx4 (Xx2!=cons(Xx3,Xx4)|member_fails(Xx1,Xx4)))& (all Xx5 (Xx2!=cons(Xx1,Xx5)))). % 2.95/3.18 all Xx1 Xx2 (member_terminates(Xx1,Xx2)<-> (all Xx3 Xx4 (Xx2!=cons(Xx3,Xx4)|member_terminates(Xx1,Xx4)))& (all Xx5 $T)). % 2.95/3.18 all Xx1 (list_succeeds(Xx1)<-> (exists Xx2 Xx3 (Xx1=cons(Xx2,Xx3)&list_succeeds(Xx3)))|Xx1=nil). % 2.95/3.18 all Xx1 (list_fails(Xx1)<-> (all Xx2 Xx3 (Xx1!=cons(Xx2,Xx3)|list_fails(Xx3)))&Xx1!=nil). % 2.95/3.18 all Xx1 (list_terminates(Xx1)<-> (all Xx2 Xx3 (Xx1!=cons(Xx2,Xx3)|list_terminates(Xx3)))). % 2.95/3.18 all Xl1 Xl2 (sub(Xl1,Xl2)<-> (all Xx (member_succeeds(Xx,Xl1)->member_succeeds(Xx,Xl2)))). % 2.95/3.18 all Xx Xl (list_succeeds(Xl)->member_terminates(Xx,Xl)). % 2.95/3.18 all Xx Xy Xl (member_succeeds(Xx,cons(Xy,Xl))&Xx!=Xy->member_succeeds(Xx,Xl)). % 2.95/3.18 all Xx Xi sub(Xi,cons(Xx,Xi)). % 2.95/3.18 all Xi Xj Xk (sub(Xi,Xj)&sub(Xj,Xk)->sub(Xi,Xk)). % 2.95/3.18 all Xl sub(nil,Xl). % 2.95/3.18 all Xx Xi Xj (sub(Xi,Xj)&member_succeeds(Xx,Xj)->sub(cons(Xx,Xi),Xj)). % 2.95/3.18 all Xi (list_succeeds(Xi)->incon_terminates(Xi)). % 2.95/3.18 all Xi (literal_list_succeeds(Xi)->list_succeeds(Xi)). % 2.95/3.18 all Xi (interpretation_succeeds(Xi)->literal_list_succeeds(Xi)& -(exists Xx (member_succeeds(p(Xx),Xi)&member_succeeds(neg(p(Xx)),Xi)))). % 2.95/3.18 all Xi (literal_list_succeeds(Xi)& -(exists Xx (member_succeeds(p(Xx),Xi)&member_succeeds(neg(p(Xx)),Xi)))->interpretation_succeeds(Xi)). % 2.95/3.18 all Xx Xi (interpretation_succeeds(Xi)& -member_succeeds(neg(p(Xx)),Xi)->interpretation_succeeds(cons(p(Xx),Xi))). % 2.95/3.18 all Xx Xi (interpretation_succeeds(Xi)&member_fails(neg(p(Xx)),Xi)->interpretation_succeeds(cons(p(Xx),Xi))). % 2.95/3.18 all Xx Xi (interpretation_succeeds(Xi)& -member_succeeds(p(Xx),Xi)->interpretation_succeeds(cons(neg(p(Xx)),Xi))). % 2.95/3.18 all Xx Xi (interpretation_succeeds(Xi)&member_fails(p(Xx),Xi)->interpretation_succeeds(cons(neg(p(Xx)),Xi))). % 2.95/3.18 interpretation_succeeds(nil). % 2.95/3.18 all Xa Xi Xj (true_succeeds(Xa,Xi,Xj)-> (interpretation_succeeds(Xi)->interpretation_succeeds(Xj))& (literal_list_succeeds(Xi)->literal_list_succeeds(Xj))&sub(Xi,Xj)). % 2.95/3.18 all Xa Xi Xj (false_succeeds(Xa,Xi,Xj)-> (interpretation_succeeds(Xi)->interpretation_succeeds(Xj))& (literal_list_succeeds(Xi)->literal_list_succeeds(Xj))&sub(Xi,Xj)). % 2.95/3.18 all Xa Xi Xj (true_succeeds(Xa,Xi,Xj)&interpretation_succeeds(Xi)->interpretation_succeeds(Xj)). % 2.95/3.18 all Xa Xi Xj (false_succeeds(Xa,Xi,Xj)&interpretation_succeeds(Xi)->interpretation_succeeds(Xj)). % 2.95/3.18 all Xa Xi Xj (true_succeeds(Xa,Xi,Xj)&literal_list_succeeds(Xi)->literal_list_succeeds(Xj)). % 2.95/3.18 all Xa Xi Xj (false_succeeds(Xa,Xi,Xj)&literal_list_succeeds(Xi)->literal_list_succeeds(Xj)). % 2.95/3.18 all Xa Xi Xj (true_succeeds(Xa,Xi,Xj)->sub(Xi,Xj)). % 2.95/3.18 all Xa Xi Xj (false_succeeds(Xa,Xi,Xj)->sub(Xi,Xj)). % 2.95/3.18 (all Xa Xi Xj ((exists Xx4 Xx5 (Xa=or(Xx4,Xx5)&true_succeeds(Xx5,Xi,Xj)& (gr(Xx5)&gr(Xi)->gr(Xj))))| (exists Xx6 Xx7 (Xa=or(Xx6,Xx7)&true_succeeds(Xx6,Xi,Xj)& (gr(Xx6)&gr(Xi)->gr(Xj))))| (exists Xx8 Xx9 Xx10 (Xa=and(Xx8,Xx9)&true_succeeds(Xx8,Xi,Xx10)& (gr(Xx8)&gr(Xi)->gr(Xx10))&true_succeeds(Xx9,Xx10,Xj)& (gr(Xx9)&gr(Xx10)->gr(Xj))))| (exists Xx11 (Xa=neg(Xx11)&false_succeeds(Xx11,Xi,Xj)))| (exists Xx12 (Xa=p(Xx12)&Xj=cons(p(Xx12),Xi)&member_fails(neg(p(Xx12)),Xi)))-> (gr(Xa)&gr(Xi)->gr(Xj))))-> (all Xa Xi Xj (true_succeeds(Xa,Xi,Xj)-> (gr(Xa)&gr(Xi)->gr(Xj)))). % 2.95/3.18 (all Xa Xi Xj ((exists Xx4 Xx5 Xx6 (Xa=or(Xx4,Xx5)&false_succeeds(Xx4,Xi,Xx6)& (gr(Xx4)&gr(Xi)->gr(Xx6))&false_succeeds(Xx5,Xx6,Xj)& (gr(Xx5)&gr(Xx6)->gr(Xj))))| (exists Xx7 Xx8 (Xa=and(Xx7,Xx8)&false_succeeds(Xx8,Xi,Xj)& (gr(Xx8)&gr(Xi)->gr(Xj))))| (exists Xx9 Xx10 (Xa=and(Xx9,Xx10)&false_succeeds(Xx9,Xi,Xj)& (gr(Xx9)&gr(Xi)->gr(Xj))))| (exists Xx11 (Xa=neg(Xx11)&true_succeeds(Xx11,Xi,Xj)))| (exists Xx12 (Xa=p(Xx12)&Xj=cons(neg(p(Xx12)),Xi)&member_fails(p(Xx12),Xi)))-> (gr(Xa)&gr(Xi)->gr(Xj))))-> (all Xa Xi Xj (false_succeeds(Xa,Xi,Xj)-> (gr(Xa)&gr(Xi)->gr(Xj)))). % 2.95/3.18 -((all Xa Xi Xj (true_succeeds(Xa,Xi,Xj)-> (gr(Xa)&gr(Xi)->gr(Xj))))& (all Xa Xi Xj (false_succeeds(Xa,Xi,Xj)-> (gr(Xa)&gr(Xi)->gr(Xj))))). % 2.95/3.18 end_of_list. % 2.95/3.18 % 2.95/3.18 ======= end of input processing ======= % 2.95/3.18 % 2.95/3.18 18 input errors were found. % 2.95/3.18 % 2.95/3.18 18 input errors were found. % 2.95/3.18 Otter interrupted % 2.95/3.18 PROOF NOT FOUND %------------------------------------------------------------------------------