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