%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : MGT047+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-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 : 600s
% DateTime : Sun Jul 17 22:26:01 EDT 2022
% Result : Theorem 19.23s 19.49s
% Output : Refutation 19.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : MGT047+1 : TPTP v8.1.0. Released v2.4.0.
% 0.00/0.11 % Command : sos-script %s
% 0.10/0.30 % Computer : n032.cluster.edu
% 0.10/0.30 % Model : x86_64 x86_64
% 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.30 % Memory : 8042.1875MB
% 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.30 % CPULimit : 300
% 0.10/0.30 % WCLimit : 600
% 0.10/0.30 % DateTime : Thu Jun 9 11:55:22 EDT 2022
% 0.10/0.31 % CPUTime :
% 0.15/0.32 ----- Otter 3.2, August 2001 -----
% 0.15/0.32 The process was started by sandbox on n032.cluster.edu,
% 0.15/0.32 Thu Jun 9 11:55:22 2022
% 0.15/0.32 The command was "./sos". The process ID is 6612.
% 0.15/0.32
% 0.15/0.32 set(prolog_style_variables).
% 0.15/0.32 set(auto).
% 0.15/0.32 dependent: set(auto1).
% 0.15/0.32 dependent: set(process_input).
% 0.15/0.32 dependent: clear(print_kept).
% 0.15/0.32 dependent: clear(print_new_demod).
% 0.15/0.32 dependent: clear(print_back_demod).
% 0.15/0.32 dependent: clear(print_back_sub).
% 0.15/0.32 dependent: set(control_memory).
% 0.15/0.32 dependent: assign(max_mem, 12000).
% 0.15/0.32 dependent: assign(pick_given_ratio, 4).
% 0.15/0.32 dependent: assign(stats_level, 1).
% 0.15/0.32 dependent: assign(pick_semantic_ratio, 3).
% 0.15/0.32 dependent: assign(sos_limit, 5000).
% 0.15/0.32 dependent: assign(max_weight, 60).
% 0.15/0.32 clear(print_given).
% 0.15/0.32
% 0.15/0.32 formula_list(usable).
% 0.15/0.32
% 0.15/0.32 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=6.
% 0.15/0.32
% 0.15/0.32 This ia a non-Horn set with equality. The strategy will be
% 0.15/0.32 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.15/0.32 unit deletion, with positive clauses in sos and nonpositive
% 0.15/0.32 clauses in usable.
% 0.15/0.32
% 0.15/0.32 dependent: set(knuth_bendix).
% 0.15/0.32 dependent: set(para_from).
% 0.15/0.32 dependent: set(para_into).
% 0.15/0.32 dependent: clear(para_from_right).
% 0.15/0.32 dependent: clear(para_into_right).
% 0.15/0.32 dependent: set(para_from_vars).
% 0.15/0.32 dependent: set(eq_units_both_ways).
% 0.15/0.32 dependent: set(dynamic_demod_all).
% 0.15/0.32 dependent: set(dynamic_demod).
% 0.15/0.32 dependent: set(order_eq).
% 0.15/0.32 dependent: set(back_demod).
% 0.15/0.32 dependent: set(lrpo).
% 0.15/0.32 dependent: set(hyper_res).
% 0.15/0.32 dependent: set(unit_deletion).
% 0.15/0.32 dependent: set(factor).
% 0.15/0.32
% 0.15/0.32 ------------> process usable:
% 0.15/0.32
% 0.15/0.32 ------------> process sos:
% 0.15/0.32 Following clause subsumed by 42 during input processing: 0 [copy,42,flip.1] {-} A=A.
% 0.15/0.32 42 back subsumes 34.
% 0.15/0.32 42 back subsumes 33.
% 0.15/0.32
% 0.15/0.32 ======= end of input processing =======
% 0.15/0.40
% 0.15/0.40 Model 1 (0.00 seconds, 0 Inserts)
% 0.15/0.40
% 0.15/0.40 Stopped by limit on number of solutions
% 0.15/0.40
% 0.15/0.40
% 0.15/0.40 -------------- Softie stats --------------
% 0.15/0.40
% 0.15/0.40 UPDATE_STOP: 300
% 0.15/0.40 SFINDER_TIME_LIMIT: 2
% 0.15/0.40 SHORT_CLAUSE_CUTOFF: 4
% 0.15/0.40 number of clauses in intial UL: 31
% 0.15/0.40 number of clauses initially in problem: 39
% 0.15/0.40 percentage of clauses intially in UL: 79
% 0.15/0.40 percentage of distinct symbols occuring in initial UL: 100
% 0.15/0.40 percent of all initial clauses that are short: 100
% 0.15/0.40 absolute distinct symbol count: 22
% 0.15/0.40 distinct predicate count: 8
% 0.15/0.40 distinct function count: 8
% 0.15/0.40 distinct constant count: 6
% 0.15/0.40
% 0.15/0.40 ---------- no more Softie stats ----------
% 0.15/0.40
% 0.15/0.40
% 0.15/0.40
% 0.15/0.40 =========== start of search ===========
% 4.22/4.41
% 4.22/4.41
% 4.22/4.41 Changing weight limit from 60 to 42.
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Model 2 (0.00 seconds, 0 Inserts)
% 4.22/4.41
% 4.22/4.41 Stopped by limit on number of solutions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Stopped by limit on insertions
% 4.22/4.41
% 4.22/4.41 Resetting weight limit to 42 after 85 givens.
% 4.22/4.41
% 4.61/4.86
% 4.61/4.86
% 4.61/4.86 Changing weight limit from 42 to 37.
% 4.61/4.86
% 4.61/4.86 Resetting weight limit to 37 after 90 givens.
% 4.61/4.86
% 5.92/6.13
% 5.92/6.13
% 5.92/6.13 Changing weight limit from 37 to 35.
% 5.92/6.13
% 5.92/6.13 Resetting weight limit to 35 after 100 givens.
% 5.92/6.13
% 8.33/8.58
% 8.33/8.58
% 8.33/8.58 Changing weight limit from 35 to 25.
% 8.33/8.58
% 8.33/8.58 Stopped by limit on insertions
% 8.33/8.58
% 8.33/8.58 Stopped by limit on insertions
% 8.33/8.58
% 8.33/8.58 Stopped by limit on insertions
% 8.33/8.58
% 8.33/8.58 Stopped by limit on insertions
% 8.33/8.58
% 8.33/8.58 Model 3 [ 2 0 2904 ] (0.00 seconds, 250000 Inserts)
% 8.33/8.58
% 8.33/8.58 Stopped by limit on insertions
% 8.33/8.58
% 8.33/8.58 Stopped by limit on insertions
% 8.33/8.58
% 8.33/8.58 Stopped by limit on insertions
% 8.33/8.58
% 8.33/8.58 Resetting weight limit to 25 after 130 givens.
% 8.33/8.58
% 10.33/10.57
% 10.33/10.57
% 10.33/10.57 Changing weight limit from 25 to 21.
% 10.33/10.57
% 10.33/10.57 Stopped by limit on insertions
% 10.33/10.57
% 10.33/10.57 Resetting weight limit to 21 after 235 givens.
% 10.33/10.57
% 10.49/10.68
% 10.49/10.68
% 10.49/10.68 Changing weight limit from 21 to 19.
% 10.49/10.68
% 10.49/10.68 Resetting weight limit to 19 after 240 givens.
% 10.49/10.68
% 11.04/11.22
% 11.04/11.22
% 11.04/11.22 Changing weight limit from 19 to 18.
% 11.04/11.22
% 11.04/11.22 Resetting weight limit to 18 after 260 givens.
% 11.04/11.22
% 11.20/11.38
% 11.20/11.38
% 11.20/11.38 Changing weight limit from 18 to 17.
% 11.20/11.38
% 11.20/11.38 Resetting weight limit to 17 after 265 givens.
% 11.20/11.38
% 14.30/14.51
% 14.30/14.51
% 14.30/14.51 Changing weight limit from 17 to 16.
% 14.30/14.51
% 14.30/14.51 Modelling stopped after 300 given clauses and 0.00 seconds
% 14.30/14.51
% 14.30/14.51
% 14.30/14.51 Resetting weight limit to 16 after 740 givens.
% 14.30/14.51
% 19.23/19.49
% 19.23/19.49 -- HEY sandbox, WE HAVE A PROOF!! --
% 19.23/19.49
% 19.23/19.49 -----> EMPTY CLAUSE at 19.04 sec ----> 29188 [hyper,29112,12,410,unit_del,28506,32,32] {-} $F.
% 19.23/19.49
% 19.23/19.49 WARNING, clause 28459 not found, proof is incomplete.
% 19.23/19.49 WARNING, clause 11932 not found, proof is incomplete.
% 19.23/19.49 Length of proof is 39. Level of proof is 13.
% 19.23/19.49
% 19.23/19.49 ---------------- PROOF ----------------
% 19.23/19.49 % SZS status Theorem
% 19.23/19.49 % SZS output start Refutation
% 19.23/19.49
% 19.23/19.49 1 [] {+} -smaller_or_equal(A,B)|smaller(A,B)|A=B.
% 19.23/19.49 2 [] {+} smaller_or_equal(A,B)| -smaller(A,B).
% 19.23/19.49 3 [] {+} smaller_or_equal(A,B)|A!=B.
% 19.23/19.49 5 [] {+} greater_or_equal(A,B)| -greater(A,B).
% 19.23/19.49 7 [] {+} -smaller(A,B)|greater(B,A).
% 19.23/19.49 8 [] {+} smaller(A,B)| -greater(B,A).
% 19.23/19.49 9 [] {+} -greater(A,B)| -greater(B,A).
% 19.23/19.49 10 [] {+} -greater(A,B)| -greater(B,C)|greater(A,C).
% 19.23/19.49 12 [] {+} -has_endowment(A)| -smaller_or_equal(age(A,B),eta)|has_immunity(A,B).
% 19.23/19.49 13 [] {+} -has_endowment(A)| -greater(age(A,B),eta)| -has_immunity(A,B).
% 19.23/19.49 17 [] {+} -organization(A)| -has_immunity(A,B)| -has_immunity(A,C)|hazard_of_mortality(A,B)=hazard_of_mortality(A,C).
% 19.23/19.49 18 [] {+} -organization(A)| -has_immunity(A,B)|has_immunity(A,C)|greater(hazard_of_mortality(A,C),hazard_of_mortality(A,B)).
% 19.23/19.49 20 [] {+} -organization(A)|has_immunity(A,B)|has_immunity(A,C)| -greater_or_equal(capability(A,C),capability(A,B))| -greater(position(A,C),position(A,B))|smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B)).
% 19.23/19.49 22 [] {+} -organization(A)| -greater(stock_of_knowledge(A,B),stock_of_knowledge(A,C))| -smaller_or_equal(internal_friction(A,B),internal_friction(A,C))|greater(capability(A,B),capability(A,C)).
% 19.23/19.49 25 [] {+} -organization(A)| -greater(external_ties(A,B),external_ties(A,C))|greater(position(A,B),position(A,C)).
% 19.23/19.49 27 [] {+} -organization(A)| -greater(age(A,B),age(A,C))|greater(stock_of_knowledge(A,B),stock_of_knowledge(A,C)).
% 19.23/19.49 28 [] {+} -organization(A)| -greater(age(A,B),age(A,C))|greater(external_ties(A,B),external_ties(A,C)).
% 19.23/19.49 29 [] {+} -organization(A)|internal_friction(A,B)=internal_friction(A,C).
% 19.23/19.49 30 [] {-} -greater(hazard_of_mortality($c5,$c2),hazard_of_mortality($c5,$c1))| -greater(hazard_of_mortality($c5,$c1),hazard_of_mortality($c5,$c3))|hazard_of_mortality($c5,$c3)!=hazard_of_mortality($c5,$c4).
% 19.23/19.49 31 [copy,30,flip.3] {+} -greater(hazard_of_mortality($c5,$c2),hazard_of_mortality($c5,$c1))| -greater(hazard_of_mortality($c5,$c1),hazard_of_mortality($c5,$c3))|hazard_of_mortality($c5,$c4)!=hazard_of_mortality($c5,$c3).
% 19.23/19.49 32 [factor,9.1.2] {+} -greater(A,A).
% 19.23/19.49 35 [] {+} smaller(A,B)|A=B|greater(A,B).
% 19.23/19.49 36 [] {+} organization($c5).
% 19.23/19.49 37 [] {-} has_endowment($c5).
% 19.23/19.49 38 [] {-} smaller_or_equal(age($c5,$c4),age($c5,$c3)).
% 19.23/19.49 39 [] {-} smaller_or_equal(age($c5,$c3),eta).
% 19.23/19.49 40 [] {+} greater(age($c5,$c2),eta).
% 19.23/19.49 41 [] {-} greater(age($c5,$c1),age($c5,$c2)).
% 19.23/19.49 42 [] {+} A=A.
% 19.23/19.49 43 [hyper,35,7] {+} A=B|greater(A,B)|greater(B,A).
% 19.23/19.49 132 [hyper,39,12,37] {-} has_immunity($c5,$c3).
% 19.23/19.49 152 [hyper,36,29] {+} internal_friction($c5,A)=internal_friction($c5,B).
% 19.23/19.49 153 [hyper,36,18,132] {+} has_immunity($c5,A)|greater(hazard_of_mortality($c5,A),hazard_of_mortality($c5,$c3)).
% 19.23/19.49 157 [hyper,38,1] {+} smaller(age($c5,$c4),age($c5,$c3))|age($c5,$c4)=age($c5,$c3).
% 19.23/19.49 176 [hyper,41,28,36] {-} greater(external_ties($c5,$c1),external_ties($c5,$c2)).
% 19.23/19.49 177 [hyper,41,27,36] {-} greater(stock_of_knowledge($c5,$c1),stock_of_knowledge($c5,$c2)).
% 19.23/19.49 198 [hyper,176,25,36] {-} greater(position($c5,$c1),position($c5,$c2)).
% 19.23/19.49 241 [hyper,40,10,41] {-} greater(age($c5,$c1),eta).
% 19.23/19.49 319 [hyper,43,13,37,132] {-} age($c5,$c3)=eta|greater(eta,age($c5,$c3)).
% 19.23/19.49 376 [para_from,43.1.1,198.1.1.2] {-} greater(position($c5,A),position($c5,$c2))|greater($c1,A)|greater(A,$c1).
% 19.23/19.49 410 [para_from,43.1.1,37.1.1] {-} has_endowment(A)|greater($c5,A)|greater(A,$c5).
% 19.23/19.49 411 [para_from,43.1.1,36.1.1] {+} organization(A)|greater($c5,A)|greater(A,$c5).
% 19.23/19.49 722 [para_into,241.1.2,43.1.1] {-} greater(age($c5,$c1),A)|greater(eta,A)|greater(A,eta).
% 19.23/19.49 2237 [hyper,152,3] {+} smaller_or_equal(internal_friction($c5,A),internal_friction($c5,B)).
% 19.23/19.49 7068 [hyper,2237,22,36,177] {-} greater(capability($c5,$c1),capability($c5,$c2)).
% 19.23/19.49 7109 [hyper,7068,5] {-} greater_or_equal(capability($c5,$c1),capability($c5,$c2)).
% 19.23/19.49 7481 [para_from,319.1.1,38.1.2] {-} smaller_or_equal(age($c5,$c4),eta)|greater(eta,age($c5,$c3)).
% 19.23/19.49 7954 [hyper,7481,12,410,unit_del,32,32] {+} greater(eta,age($c5,$c3))|has_immunity($c5,$c4).
% 19.23/19.49 9744 [hyper,722,10,722,unit_del,32,32,factor_simp] {-} greater(age($c5,$c1),A)|greater(A,eta).
% 19.23/19.49 10570 [hyper,153,13,410,9744,unit_del,32,32,32] {-} greater(hazard_of_mortality($c5,$c1),hazard_of_mortality($c5,$c3)).
% 19.23/19.49 10573 [hyper,153,13,410,40,unit_del,32,32] {+} greater(hazard_of_mortality($c5,$c2),hazard_of_mortality($c5,$c3)).
% 19.23/19.49 10944 [para_from,157.2.1,12.2.1,unit_del,37,39] {+} has_immunity($c5,$c4)|smaller(age($c5,$c4),age($c5,$c3)).
% 19.23/19.49 11967 [factor,11932.1.3,unit_del,32,32] {-} -has_immunity($c5,$c1).
% 19.23/19.49 12050 [para_into,10573.1.2,17.4.1,unit_del,36,132] {+} greater(hazard_of_mortality($c5,$c2),hazard_of_mortality($c5,A))| -has_immunity($c5,A).
% 19.23/19.49 18162 [hyper,10944,7] {+} has_immunity($c5,$c4)|greater(age($c5,$c3),age($c5,$c4)).
% 19.23/19.49 18238 [para_into,12050.1.1,17.4.1,unit_del,36] {-} greater(hazard_of_mortality($c5,A),hazard_of_mortality($c5,B))| -has_immunity($c5,B)| -has_immunity($c5,$c2)| -has_immunity($c5,A).
% 19.23/19.49 18258 [factor,18238.2.4,unit_del,32,factor_simp] {+} -has_immunity($c5,$c2).
% 19.23/19.49 19438 [hyper,376,20,411,7109,unit_del,32,32,18258,11967,32,32] {+} smaller(hazard_of_mortality($c5,$c1),hazard_of_mortality($c5,$c2)).
% 19.23/19.49 20064 [hyper,19438,7] {+} greater(hazard_of_mortality($c5,$c2),hazard_of_mortality($c5,$c1)).
% 19.23/19.49 28460 [factor,28459.1.2,unit_del,32] {+} hazard_of_mortality($c5,A)=hazard_of_mortality($c5,$c3)| -has_immunity($c5,A).
% 19.23/19.49 28506 [para_from,28460.1.1,31.3.1,unit_del,20064,10570,42] {-} -has_immunity($c5,$c4).
% 19.23/19.49 28512 [hyper,28506,18162] {-} greater(age($c5,$c3),age($c5,$c4)).
% 19.23/19.49 28514 [hyper,28506,7954] {-} greater(eta,age($c5,$c3)).
% 19.23/19.49 28771 [hyper,28512,10,28514] {-} greater(eta,age($c5,$c4)).
% 19.23/19.49 29074 [hyper,28771,8] {-} smaller(age($c5,$c4),eta).
% 19.23/19.49 29112 [hyper,29074,2] {-} smaller_or_equal(age($c5,$c4),eta).
% 19.23/19.49 29188 [hyper,29112,12,410,unit_del,28506,32,32] {-} $F.
% 19.23/19.49
% 19.23/19.49 % SZS output end Refutation
% 19.23/19.49 ------------ end of proof -------------
% 19.23/19.49
% 19.23/19.49
% 19.23/19.49 Search stopped by max_proofs option.
% 19.23/19.49
% 19.23/19.49
% 19.23/19.49 Search stopped by max_proofs option.
% 19.23/19.49
% 19.23/19.49 ============ end of search ============
% 19.23/19.49
% 19.23/19.49 ----------- soft-scott stats ----------
% 19.23/19.49
% 19.23/19.49 true clauses given 759 (31.6%)
% 19.23/19.49 false clauses given 1646
% 19.23/19.49
% 19.23/19.49 FALSE TRUE
% 19.23/19.49 5 0 1
% 19.23/19.49 6 0 2
% 19.23/19.49 7 11 1
% 19.23/19.49 9 10 9
% 19.23/19.49 10 3 1
% 19.23/19.49 11 98 155
% 19.23/19.49 12 12 1534
% 19.23/19.49 13 459 556
% 19.23/19.49 14 260 77
% 19.23/19.49 15 696 69
% 19.23/19.49 16 214 95
% 19.23/19.49 tot: 1763 2500 (58.6% true)
% 19.23/19.49
% 19.23/19.49
% 19.23/19.49 Model 3 [ 2 -293 2904 ] (0.00 seconds, 250000 Inserts)
% 19.23/19.49
% 19.23/19.49 That finishes the proof of the theorem.
% 19.23/19.49
% 19.23/19.49 Process 6612 finished Thu Jun 9 11:55:42 2022
%------------------------------------------------------------------------------