%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX240-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n022.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 Apr 29 02:38:10 PM UTC 2026 % Result : Unsatisfiable 27.82s 28.20s % Output : Refutation 27.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX240-1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.15/0.34 % Computer : n022.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Wed Apr 29 03:05:36 EDT 2026 % 0.15/0.34 % CPUTime : % 5.02/5.32 ============================== Prover9 =============================== % 5.02/5.32 Prover9 (32) version 2009-11A, November 2009. % 5.02/5.32 Process 1224 was started by sandbox2 on n022.cluster.edu, % 5.02/5.32 Wed Apr 29 03:05:36 2026 % 5.02/5.32 The command was "/export/starexec/sandbox2/solver/bin/prover9 -t 300 -f /tmp/Prover9_1059_n022.cluster.edu". % 5.02/5.32 ============================== end of head =========================== % 5.02/5.32 % 5.02/5.32 ============================== INPUT ================================= % 5.02/5.32 % 5.02/5.32 % Reading from file /tmp/Prover9_1059_n022.cluster.edu % 5.02/5.32 % 5.02/5.32 set(prolog_style_variables). % 5.02/5.32 set(auto2). % 5.02/5.32 % set(auto2) -> set(auto). % 5.02/5.32 % set(auto) -> set(auto_inference). % 5.02/5.32 % set(auto) -> set(auto_setup). % 5.02/5.32 % set(auto_setup) -> set(predicate_elim). % 5.02/5.32 % set(auto_setup) -> assign(eq_defs, unfold). % 5.02/5.32 % set(auto) -> set(auto_limits). % 5.02/5.32 % set(auto_limits) -> assign(max_weight, "100.000"). % 5.02/5.32 % set(auto_limits) -> assign(sos_limit, 20000). % 5.02/5.32 % set(auto) -> set(auto_denials). % 5.02/5.32 % set(auto) -> set(auto_process). % 5.02/5.32 % set(auto2) -> assign(new_constants, 1). % 5.02/5.32 % set(auto2) -> assign(fold_denial_max, 3). % 5.02/5.32 % set(auto2) -> assign(max_weight, "200.000"). % 5.02/5.32 % set(auto2) -> assign(max_hours, 1). % 5.02/5.32 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 5.02/5.32 % set(auto2) -> assign(max_seconds, 0). % 5.02/5.32 % set(auto2) -> assign(max_minutes, 5). % 5.02/5.32 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 5.02/5.32 % set(auto2) -> set(sort_initial_sos). % 5.02/5.32 % set(auto2) -> assign(sos_limit, -1). % 5.02/5.32 % set(auto2) -> assign(lrs_ticks, 3000). % 5.02/5.32 % set(auto2) -> assign(max_megs, 400). % 5.02/5.32 % set(auto2) -> assign(stats, some). % 5.02/5.32 % set(auto2) -> clear(echo_input). % 5.02/5.32 % set(auto2) -> set(quiet). % 5.02/5.32 % set(auto2) -> clear(print_initial_clauses). % 5.02/5.32 % set(auto2) -> clear(print_given). % 5.02/5.32 assign(lrs_ticks,-1). % 5.02/5.32 assign(sos_limit,10000). % 5.02/5.32 assign(order,kbo). % 5.02/5.32 set(lex_order_vars). % 5.02/5.32 clear(print_given). % 5.02/5.32 % 5.02/5.32 % formulas(sos). % not echoed (88 formulas) % 5.02/5.32 % 5.02/5.32 ============================== end of input ========================== % 5.02/5.32 % 5.02/5.32 % From the command line: assign(max_seconds, 300). % 5.02/5.32 % 5.02/5.32 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 5.02/5.32 % 5.02/5.32 % Formulas that are not ordinary clauses: % 5.02/5.32 % 5.02/5.32 ============================== end of process non-clausal formulas === % 5.02/5.32 % 5.02/5.32 ============================== PROCESS INITIAL CLAUSES =============== % 5.02/5.32 % 5.02/5.32 ============================== PREDICATE ELIMINATION ================= % 5.02/5.32 % 5.02/5.32 ============================== end predicate elimination ============= % 5.02/5.32 % 5.02/5.32 Auto_denials: % 5.02/5.32 % copying label goal to answer in negative clause % 5.02/5.32 % 5.02/5.32 Term ordering decisions: % 5.02/5.32 Function symbol KB weights: bfalse=1. btrue=1. fF=1. skip=1. tT=1. zero=1. l=1. nil=1. h=1. eq4=1. eq3=1. assign=1. nand=1. seq=1. eq2=1. run=1. eval=1. eq=1. elem=1. andb=1. cons=1. del=1. eq5=1. orb=1. impl=1. prop=1. var=1. typeCorrect=1. secret=1. high=1. low=1. notb=1. suc=1. ifThenElse=1. aux=1. aux2=1. aux3=1. % 5.02/5.32 % 5.02/5.32 ============================== end of process initial clauses ======== % 5.02/5.32 % 5.02/5.32 ============================== CLAUSES FOR SEARCH ==================== % 5.02/5.32 % 5.02/5.32 ============================== end of clauses for search ============= % 5.02/5.32 % 5.02/5.32 ============================== SEARCH ================================ % 5.02/5.32 % 5.02/5.32 % Starting search at 0.01 seconds. % 5.02/5.32 % 5.02/5.32 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 64 (0.00 of 0.39 sec). % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=48.000, iters=3348 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=47.000, iters=3384 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=46.000, iters=3334 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=45.000, iters=3357 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=44.000, iters=3457 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=43.000, iters=3370 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=42.000, iters=3334 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=40.000, iters=3477 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=38.000, iters=3386 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=37.000, iters=3336 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=36.000, iters=3504 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=35.000, iters=3397 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=34.000, iters=3344 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=33.000, iters=3420 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=32.000, iters=3769 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=31.000, iters=3512 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=30.000, iters=3334 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=28.000, iters=3423 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=27.000, iters=3404 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=26.000, iters=3414 % 5.02/5.32 % 5.02/5.32 Low Water (keep): wt=25.000, iters=3695 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=5493, wt=59.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=6217, wt=58.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=6007, wt=57.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=6262, wt=56.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=6006, wt=55.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=6264, wt=54.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=6004, wt=53.000 % 27.82/28.20 % 27.82/28.20 Low Water (keep): wt=23.000, iters=3334 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=6378, wt=52.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=6001, wt=51.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=6364, wt=50.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=5996, wt=49.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=6374, wt=48.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=5995, wt=47.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=2642, wt=39.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=8801, wt=38.000 % 27.82/28.20 % 27.82/28.20 Low Water (keep): wt=22.000, iters=3344 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=9186, wt=37.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=9245, wt=36.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=9185, wt=35.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=9479, wt=34.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=9652, wt=33.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=10312, wt=32.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=10306, wt=31.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=10302, wt=30.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=11050, wt=29.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=15420, wt=20.000 % 27.82/28.20 % 27.82/28.20 Low Water (displace): id=15445, wt=19.000 % 27.82/28.20 % 27.82/28.20 Low Water (keep): wt=21.000, iters=3394 % 27.82/28.20 % 27.82/28.20 ============================== PROOF ================================= % 27.82/28.20 % SZS status Unsatisfiable % 27.82/28.20 % SZS output start Refutation % 27.82/28.20 % 27.82/28.20 % Proof 1 at 26.24 (+ 0.72) seconds: goal. % 27.82/28.20 % Length of proof is 67. % 27.82/28.20 % Level of proof is 10. % 27.82/28.20 % Maximum clause weight is 30.000. % 27.82/28.20 % Given clauses 4284. % 27.82/28.20 % 27.82/28.20 2 secret(fF) = bfalse # label(axiom_012) # label(axiom). [assumption]. % 27.82/28.20 4 notb(bfalse) = btrue # label(axiom_014) # label(axiom). [assumption]. % 27.82/28.20 5 l = low(zero) # label(axiom_015) # label(axiom). [assumption]. % 27.82/28.20 6 low(zero) = l. [copy(5),flip(a)]. % 27.82/28.20 7 h = high(zero) # label(axiom_018) # label(axiom). [assumption]. % 27.82/28.20 8 high(zero) = h. [copy(7),flip(a)]. % 27.82/28.20 9 typeCorrect(skip) = btrue # label(axiom_033) # label(axiom). [assumption]. % 27.82/28.20 10 orb(btrue,A) = btrue # label(axiom_006) # label(axiom). [assumption]. % 27.82/28.20 11 orb(bfalse,A) = A # label(axiom_007) # label(axiom). [assumption]. % 27.82/28.20 12 impl(btrue,A) = A # label(axiom_016) # label(axiom). [assumption]. % 27.82/28.20 14 elem(A,nil) = bfalse # label(axiom_019) # label(axiom). [assumption]. % 27.82/28.20 15 del(A,nil) = nil # label(axiom_021) # label(axiom). [assumption]. % 27.82/28.20 16 andb(btrue,A) = A # label(axiom_023) # label(axiom). [assumption]. % 27.82/28.20 19 eval(A,fF) = bfalse # label(axiom_027) # label(axiom). [assumption]. % 27.82/28.20 20 run(A,skip) = A # label(axiom_029) # label(axiom). [assumption]. % 27.82/28.20 23 eq5(bfalse,btrue) = bfalse # label(axiom_041) # label(axiom). [assumption]. % 27.82/28.20 27 eq3(A,A) = btrue # label(axiom_084) # label(axiom). [assumption]. % 27.82/28.20 29 eq5(A,A) = btrue # label(axiom_086) # label(axiom). [assumption]. % 27.82/28.20 43 eq2(high(A),low(B)) = bfalse # label(axiom_058) # label(axiom). [assumption]. % 27.82/28.20 44 eq2(low(A),high(B)) = bfalse # label(axiom_059) # label(axiom). [assumption]. % 27.82/28.20 49 eval(A,var(B)) = elem(B,A) # label(axiom_028) # label(axiom). [assumption]. % 27.82/28.20 50 elem(A,B) = eval(B,var(A)). [copy(49),flip(a)]. % 27.82/28.20 55 aux(A,B,C,btrue) = del(A,C) # label(axiom) # label(axiom). [assumption]. % 27.82/28.20 57 aux2(A,B,C,bfalse) = del(B,A) # label(axiom_003) # label(axiom). [assumption]. % 27.82/28.20 58 typeCorrect(assign(low(A),B)) = notb(secret(B)) # label(axiom_035) # label(axiom). [assumption]. % 27.82/28.20 59 eq3(var(A),var(B)) = eq2(A,B) # label(axiom_045) # label(axiom). [assumption]. % 27.82/28.20 60 eq2(A,B) = eq3(var(A),var(B)). [copy(59),flip(a)]. % 27.82/28.20 69 aux3(A,B,C,D,btrue) = run(A,C) # label(axiom_004) # label(axiom). [assumption]. % 27.82/28.20 70 aux3(A,B,C,D,bfalse) = run(A,D) # label(axiom_005) # label(axiom). [assumption]. % 27.82/28.20 73 typeCorrect(seq(A,B)) = andb(typeCorrect(A),typeCorrect(B)) # label(axiom_036) # label(axiom). [assumption]. % 27.82/28.20 74 andb(typeCorrect(A),typeCorrect(B)) = typeCorrect(seq(A,B)). [copy(73),flip(a)]. % 27.82/28.20 82 typeCorrect(ifThenElse(A,B,C)) = andb(typeCorrect(B),typeCorrect(C)) # label(axiom_037) # label(axiom). [assumption]. % 27.82/28.20 83 typeCorrect(ifThenElse(A,B,C)) = typeCorrect(seq(B,C)). [copy(82),rewrite([74(5)])]. % 27.82/28.20 84 elem(A,cons(B,C)) = orb(eq2(B,A),elem(A,C)) # label(axiom_020) # label(axiom). [assumption]. % 27.82/28.21 85 orb(eq3(var(A),var(B)),eval(C,var(B))) = eval(cons(A,C),var(B)). [copy(84),rewrite([50(2),60(4),50(7)]),flip(a)]. % 27.82/28.21 86 del(A,cons(B,C)) = aux(A,B,C,eq2(A,B)) # label(axiom_022) # label(axiom). [assumption]. % 27.82/28.21 87 aux(A,B,C,eq3(var(A),var(B))) = del(A,cons(B,C)). [copy(86),rewrite([60(3)]),flip(a)]. % 27.82/28.21 88 run(A,assign(B,C)) = aux2(A,B,C,eval(A,C)) # label(axiom_030) # label(axiom). [assumption]. % 27.82/28.21 89 aux2(A,B,C,eval(A,C)) = run(A,assign(B,C)). [copy(88),flip(a)]. % 27.82/28.21 92 run(A,ifThenElse(B,C,D)) = aux3(A,B,C,D,eval(A,B)) # label(axiom_032) # label(axiom). [assumption]. % 27.82/28.21 93 aux3(A,B,C,D,eval(A,B)) = run(A,ifThenElse(B,C,D)). [copy(92),flip(a)]. % 27.82/28.21 94 prop(A,B) = impl(typeCorrect(A),eq5(elem(l,run(B,A)),elem(l,run(cons(h,B),A)))) # label(axiom_038) # label(axiom). [assumption]. % 27.82/28.21 95 prop(A,B) = impl(typeCorrect(A),eq5(eval(run(B,A),var(l)),eval(run(cons(h,B),A),var(l)))). [copy(94),rewrite([50(5),50(11)])]. % 27.82/28.21 96 eq5(prop(A,B),bfalse) != btrue # label(goal) # label(negated_conjecture) # answer(goal). [assumption]. % 27.82/28.21 97 eq5(impl(typeCorrect(A),eq5(eval(run(B,A),var(l)),eval(run(cons(h,B),A),var(l)))),bfalse) != btrue # answer(goal). [copy(96),rewrite([95(1)])]. % 27.82/28.21 109 eval(nil,var(A)) = bfalse. [back_rewrite(14),rewrite([50(2)])]. % 27.82/28.21 110 eq3(var(low(A)),var(high(B))) = bfalse. [back_rewrite(44),rewrite([60(3)])]. % 27.82/28.21 111 eq3(var(high(A)),var(low(B))) = bfalse. [back_rewrite(43),rewrite([60(3)])]. % 27.82/28.21 117 typeCorrect(assign(l,A)) = notb(secret(A)). [para(6(a,1),58(a,1,1,1))]. % 27.82/28.21 129 typeCorrect(seq(skip,A)) = typeCorrect(A). [para(9(a,1),74(a,1,1)),rewrite([16(3)]),flip(a)]. % 27.82/28.21 140 eval(cons(A,B),var(A)) = btrue. [para(27(a,1),85(a,1,1)),rewrite([10(4)]),flip(a)]. % 27.82/28.21 143 del(A,cons(A,B)) = del(A,B). [para(27(a,1),87(a,1,4)),rewrite([55(2)]),flip(a)]. % 27.82/28.21 147 run(A,assign(B,fF)) = del(B,A). [para(19(a,1),89(a,1,4)),rewrite([57(3)]),flip(a)]. % 27.82/28.21 158 eq5(impl(typeCorrect(seq(A,B)),eq5(eval(run(C,ifThenElse(D,A,B)),var(l)),eval(run(cons(h,C),ifThenElse(D,A,B)),var(l)))),bfalse) != btrue # answer(goal). [para(83(a,1),97(a,1,1,1))]. % 27.82/28.21 265 eq3(var(l),var(high(A))) = bfalse. [para(6(a,1),110(a,1,1,1))]. % 27.82/28.21 272 eq3(var(high(A)),var(l)) = bfalse. [para(6(a,1),111(a,1,2,1))]. % 27.82/28.21 332 eval(cons(A,cons(B,C)),var(B)) = orb(eq3(var(A),var(B)),btrue). [para(140(a,1),85(a,1,2)),flip(a)]. % 27.82/28.21 336 run(cons(A,B),ifThenElse(var(A),C,D)) = run(cons(A,B),C). [para(140(a,1),93(a,1,5)),rewrite([69(4)]),flip(a)]. % 27.82/28.21 351 eq3(var(l),var(h)) = bfalse. [para(8(a,1),265(a,1,2,1))]. % 27.82/28.21 366 eval(cons(l,A),var(h)) = eval(A,var(h)). [para(351(a,1),85(a,1,1)),rewrite([11(5)]),flip(a)]. % 27.82/28.21 376 eq3(var(h),var(l)) = bfalse. [para(8(a,1),272(a,1,1,1))]. % 27.82/28.21 718 aux3(cons(l,A),var(h),B,C,eval(A,var(h))) = run(cons(l,A),ifThenElse(var(h),B,C)). [para(366(a,1),93(a,1,5))]. % 27.82/28.21 775 eq5(impl(typeCorrect(A),eq5(eval(run(B,ifThenElse(C,skip,A)),var(l)),eval(run(cons(h,B),ifThenElse(C,skip,A)),var(l)))),bfalse) != btrue # answer(goal). [para(129(a,1),158(a,1,1,1))]. % 27.82/28.21 12410 run(cons(l,nil),ifThenElse(var(h),A,B)) = run(cons(l,nil),B). [para(109(a,1),718(a,1,5)),rewrite([70(7)]),flip(a)]. % 27.82/28.21 13490 eq5(impl(typeCorrect(A),eq5(eval(run(cons(l,nil),A),var(l)),btrue)),bfalse) != btrue # answer(goal). [para(12410(a,1),775(a,1,1,2,1,1)),rewrite([336(18),20(15),332(16),376(13),11(11)])]. % 27.82/28.21 13497 eq5(impl(typeCorrect(assign(A,fF)),eq5(eval(del(A,cons(l,nil)),var(l)),btrue)),bfalse) != btrue # answer(goal). [para(147(a,1),13490(a,1,1,2,1,1))]. % 27.82/28.21 19269 $F # answer(goal). [para(117(a,1),13497(a,1,1,1)),rewrite([2(2),4(2),143(6),15(4),109(5),23(4),12(3),29(3)]),xx(a)]. % 27.82/28.21 % 27.82/28.21 % SZS output end Refutation % 27.82/28.21 ============================== end of proof ========================== % 27.82/28.21 % 27.82/28.21 ============================== STATISTICS ============================ % 27.82/28.21 % 27.82/28.21 Given=4284. Generated=752465. Kept=19248. proofs=1. % 27.82/28.21 Usable=4217. Sos=9999. Demods=6634. Limbo=1, Disabled=5119. Hints=0. % 27.82/28.21 Megabytes=22.55. % 27.82/28.21 User_CPU=26.24, System_CPU=0.72, Wall_clock=27. % 27.82/28.21 % 27.82/28.21 ============================== end of statistics ===================== % 27.82/28.21 % 27.82/28.21 ============================== end of search ========================= % 27.82/28.21 % 27.82/28.21 THEOREM PROVED % 27.82/28.21 % SZS status Unsatisfiable % 27.82/28.21 % 27.82/28.21 Exiting with 1 proof. % 27.82/28.21 % 27.82/28.21 Process 1224 exit (max_proofs) Wed Apr 29 03:06:03 2026 % 27.82/28.21 Prover9 interrupted %------------------------------------------------------------------------------