%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : SWV384+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n010.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 : 600s % DateTime : Wed Jul 20 21:38:17 EDT 2022 % Result : Unknown 0.20s 0.36s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV384+1 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.12 % Command : sos-script %s % 0.12/0.34 % Computer : n010.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 : 600 % 0.12/0.34 % DateTime : Tue Jun 14 16:56:09 EDT 2022 % 0.12/0.34 % CPUTime : % 0.20/0.36 ----- Otter 3.2, August 2001 ----- % 0.20/0.36 The process was started by sandbox on n010.cluster.edu, % 0.20/0.36 Tue Jun 14 16:56:09 2022 % 0.20/0.36 The command was "./sos". The process ID is 23790. % 0.20/0.36 % 0.20/0.36 set(prolog_style_variables). % 0.20/0.36 set(auto). % 0.20/0.36 dependent: set(auto1). % 0.20/0.36 dependent: set(process_input). % 0.20/0.36 dependent: clear(print_kept). % 0.20/0.36 dependent: clear(print_new_demod). % 0.20/0.36 dependent: clear(print_back_demod). % 0.20/0.36 dependent: clear(print_back_sub). % 0.20/0.36 dependent: set(control_memory). % 0.20/0.36 dependent: assign(max_mem, 12000). % 0.20/0.36 dependent: assign(pick_given_ratio, 4). % 0.20/0.36 dependent: assign(stats_level, 1). % 0.20/0.36 dependent: assign(pick_semantic_ratio, 3). % 0.20/0.36 dependent: assign(sos_limit, 5000). % 0.20/0.36 dependent: assign(max_weight, 60). % 0.20/0.36 clear(print_given). % 0.20/0.36 % 0.20/0.36 formula_list(usable). % 0.20/0.36 % 0.20/0.36 ERROR, the 6 terms/operators in the following sequence are OK, but they % 0.20/0.36 could not be combined into a single term with special operators. % 0.20/0.36 the % 0.20/0.36 induction % 0.20/0.36 principle % 0.20/0.36 used % 0.20/0.36 in % 0.20/0.36 Coq % 0.20/0.36 % 0.20/0.36 The context of the bad sequence is: % 0.20/0.36 % 0.20/0.36 /*---- % 0.20/0.36 Explanation about induction % 0.20/0.36 =========================== % 0.20/0.36 % 0.20/0.36 In order to prove lemma_not_check_not_phi we use the following induction % 0.20/0.36 principle: ( ***HERE*** the induction principle used in Coq) % 0.20/0.36 ===================== % 0.20/0.36 let s/1 be the successor function defined on some set S and let =</2 be the % 0.20/0.36 predicate that satisfies the following axioms: % 0.20/0.36 % 0.20/0.36 1) x =< x % 0.20/0.36 2) x =< y -> x =< s(y) % 0.20/0.36 % 0.20/0.36 Note that our predicate succ/2 satisfies those two axioms % 0.20/0.36 % 0.20/0.36 The induction principle: (V = for eVery % 0.20/0.36 % 0.20/0.36 Vx ( (P(x) and Vy (x =< y -> (P(y) -> P(s(y)))) -> Vy (x=<y -> P(y)) ) % 0.20/0.36 ====================== % 0.20/0.36 % 0.20/0.36 Let P(x) == ~(checked(x)) or ~(ok(x)) and let =</2 == succ/2 % 0.20/0.36 % 0.20/0.36 Then, in order to confirm correctness of lemma_not_check_not_phi we have to % 0.20/0.36 only verify "Vy (x =< y -> (P(y) -> P(s(y))))" of the induction principle, % 0.20/0.36 in other words we need to prove that: % 0.20/0.36 % 0.20/0.36 all(CPQ1, all(CPQ2, succ(CPQ1, CPQ2) => ( ( ~(checked(CPQ2)) or ~(ok(CPQ2)) ) => ( ~(checked(s(CPQ2))) or ~(ok(s(CPQ2))) ) ) )), (1) % 0.20/0.36 % 0.20/0.36 where s(CPQ2) in the immediate successor of CPQ2. % 0.20/0.36 % 0.20/0.36 ERROR, the 3 terms/operators in the following sequence are OK, but they % 0.20/0.36 could not be combined into a single term with special operators. % 0.20/0.36 ~(checked(CPQ2)) % 0.20/0.36 or % 0.20/0.36 ~(ok(CPQ2)) % 0.20/0.36 % 0.20/0.36 The context of the bad sequence is: % 0.20/0.36 % 0.20/0.36 all(CPQ2, ( ***HERE*** ~(checked(CPQ2)) or ~(ok(CPQ2)) ) => ( ~(checked(s(CPQ2))) or ~(ok(s(CPQ2))) ) ) (2) % 0.20/0.36 % 0.20/0.36 is a valid formula. % 0.20/0.36 % 0.20/0.36 ERROR, the 9 terms/operators in the following sequence are OK, but they % 0.20/0.36 could not be combined into a single term with special operators. % 0.20/0.36 The % 0.20/0.36 validity % 0.20/0.36 of % 0.20/0.36 formula % 0.20/0.36 2 % 0.20/0.36 is % 0.20/0.36 proved % 0.20/0.36 in % 0.20/0.36 lemma_not_min_elem_not_check_induction02 % 0.20/0.36 % 0.20/0.36 The context of the bad sequence is: % 0.20/0.36 ***HERE*** % 0.20/0.36 The validity of formula (2) is proved in % 0.20/0.36 lemma_not_min_elem_not_check_induction02, % 0.20/0.36 so here we have included it as a valid formula % 0.20/0.36 % 0.20/0.36 lemma_not_min_elem_not_check_induction02 proves the validity of formula (1) % 0.20/0.36 and thus, since (1) is valid we can conclude that the following formula holds: % 0.20/0.36 % 0.20/0.36 Vx ( P(x) -> Vy (x=<y -> P(y)) ) % 0.20/0.36 % 0.20/0.36 or in our example: % 0.20/0.36 % 0.20/0.36 all(CPQ, (~(checked(CPQ)) or ~(ok(CPQ))) => all(CPQ1, succ(CPQ, CPQ1) => ( ~(ok(CPQ1)) or ~(checked(CPQ1)) )) % 0.20/0.36 % 0.20/0.36 which completes the inductive proof of lemma_not_min_elem_not_check_induction % 0.20/0.36 ----*/ % 0.20/0.36 % 0.20/0.36 % 0.20/0.36 % 0.20/0.36 ( all U V W X Y Z ( % 0.20/0.36 ( succ_cpq(triple(U,V,W),triple(X,Y,Z)) % 0.20/0.36 -> ( ( -check_cpq(triple(X,Y,Z)) % 0.20/0.36 | -ok(triple(X,Y,Z)) ) % 0.20/0.36 -> ( -check_cpq(im_succ_cpq(triple(X,Y,Z))) % 0.20/0.36 | -ok(im_succ_cpq(triple(X,Y,Z))) ) ) ) ) ) % 0.20/0.36 -> ( all X1 X2 X3 ( % 0.20/0.36 ( ( -check_cpq(triple(X1,X2,X3)) % 0.20/0.36 | -ok(triple(X1,X2,X3)) ) % 0.20/0.36 -> ( all X4 X5 X6 ( % 0.20/0.36 ( succ_cpq(triple(X1,X2,X3),triple(X4,X5,X6)) % 0.20/0.36 -> ( -ok(triple(X4,X5,X6)) % 0.20/0.36 | -check_cpq(triple(X4,X5,X6)) ) ) ) ) ) ) ). % 0.20/0.36 % 0.20/0.36 ======= end of input processing ======= % 0.20/0.36 % 0.20/0.36 3 input errors were found. % 0.20/0.36 % 0.20/0.36 3 input errors were found. %------------------------------------------------------------------------------