%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NLP257+1 : TPTP v8.2.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n021.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 : Mon Jun 24 12:01:59 EDT 2024 % Result : Theorem 116.74s 116.80s % Output : CNFRefutation 116.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NLP257+1 : TPTP v8.2.0. Released v2.4.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sat Jun 22 04:22:54 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 116.74/116.77 %------------------------------------------- % 116.74/116.77 % File :CSE---1.7 % 116.74/116.77 % Problem :theBenchmark % 116.74/116.77 % Transform :cnf % 116.74/116.77 % Format :tptp:raw % 116.74/116.77 % Command :java -jar mcs_scs.jar %d %s % 116.74/116.77 % 116.74/116.77 % Result :Theorem 116.120000s % 116.74/116.77 % Output :CNFRefutation 116.120000s % 116.74/116.77 %------------------------------------------- % 116.74/116.78 %-------------------------------------------------------------------------- % 116.74/116.78 % File : NLP257+1 : TPTP v8.2.0. Released v2.4.0. % 116.74/116.78 % Domain : Natural Language Processing % 116.74/116.78 % Problem : Vincent believes that every man smokes, problem 38 % 116.74/116.78 % Version : [Bos00b] axioms. % 116.74/116.78 % English : Eliminating non-informative interpretations in the statement % 116.74/116.78 % "Vincent believes that every man smokes. Jules is a man. % 116.74/116.78 % Vincent believes that jules smokes." % 116.74/116.78 % 116.74/116.78 % Refs : [Bos00a] Bos (2000), DORIS: Discourse Oriented Representation a % 116.74/116.78 % [Bos00b] Bos (2000), Applied Theorem Proving - Natural Language % 116.74/116.78 % Source : [Bos00b] % 116.74/116.78 % Names : doris234 [Bos00b] % 116.74/116.78 % 116.74/116.78 % Status : Theorem % 116.74/116.78 % Rating : 0.19 v8.2.0, 0.17 v7.5.0, 0.22 v7.4.0, 0.10 v7.3.0, 0.17 v7.2.0, 0.14 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.12 v6.2.0, 0.16 v6.1.0, 0.30 v5.5.0, 0.37 v5.4.0, 0.39 v5.3.0, 0.44 v5.2.0, 0.20 v5.1.0, 0.24 v5.0.0, 0.25 v4.1.0, 0.30 v4.0.1, 0.26 v4.0.0, 0.29 v3.7.0, 0.14 v3.5.0, 0.00 v3.4.0, 0.17 v3.3.0, 0.11 v3.2.0, 0.33 v2.7.0, 0.00 v2.4.0 % 116.74/116.78 % Syntax : Number of formulae : 72 ( 0 unt; 0 def) % 116.74/116.78 % Number of atoms : 253 ( 3 equ) % 116.74/116.78 % Maximal formula atoms : 66 ( 3 avg) % 116.74/116.78 % Number of connectives : 189 ( 8 ~; 0 |; 108 &) % 116.74/116.78 % ( 0 <=>; 73 =>; 0 <=; 0 <~>) % 116.74/116.78 % Maximal formula depth : 55 ( 6 avg) % 116.74/116.78 % Maximal term depth : 1 ( 1 avg) % 116.74/116.78 % Number of predicates : 37 ( 36 usr; 0 prp; 1-4 aty) % 116.74/116.78 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 116.74/116.78 % Number of variables : 215 ( 190 !; 25 ?) % 116.74/116.78 % SPC : FOF_THM_RFO_SEQ % 116.74/116.78 % 116.74/116.78 % Comments : % 116.74/116.78 %-------------------------------------------------------------------------- % 116.74/116.78 fof(ax1,axiom, % 116.74/116.78 ! [U,V] : % 116.74/116.78 ( jules_forename(U,V) % 116.74/116.78 => forename(U,V) ) ). % 116.74/116.78 % 116.74/116.78 fof(ax2,axiom, % 116.74/116.78 ! [U,V] : % 116.74/116.78 ( vincent_forename(U,V) % 116.74/116.78 => forename(U,V) ) ). % 116.74/116.78 % 116.74/116.78 fof(ax3,axiom, % 116.74/116.78 ! [U,V] : % 116.74/116.79 ( relname(U,V) % 116.74/116.79 => relation(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax4,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( forename(U,V) % 116.74/116.79 => relname(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax5,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( man(U,V) % 116.74/116.79 => male(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax6,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( human_person(U,V) % 116.74/116.79 => animate(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax7,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( human_person(U,V) % 116.74/116.79 => human(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax8,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( organism(U,V) % 116.74/116.79 => living(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax9,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( organism(U,V) % 116.74/116.79 => impartial(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax10,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( entity(U,V) % 116.74/116.79 => existent(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax11,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( entity(U,V) % 116.74/116.79 => specific(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax12,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( entity(U,V) % 116.74/116.79 => thing(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax13,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( organism(U,V) % 116.74/116.79 => entity(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax14,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( human_person(U,V) % 116.74/116.79 => organism(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax15,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( man(U,V) % 116.74/116.79 => human_person(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax16,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( state(U,V) % 116.74/116.79 => event(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax17,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( state(U,V) % 116.74/116.79 => eventuality(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax18,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( abstraction(U,V) % 116.74/116.79 => unisex(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax19,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( abstraction(U,V) % 116.74/116.79 => general(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax20,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( abstraction(U,V) % 116.74/116.79 => nonhuman(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax21,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( abstraction(U,V) % 116.74/116.79 => thing(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax22,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( relation(U,V) % 116.74/116.79 => abstraction(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax23,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( proposition(U,V) % 116.74/116.79 => relation(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax24,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( eventuality(U,V) % 116.74/116.79 => unisex(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax25,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( eventuality(U,V) % 116.74/116.79 => nonexistent(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax26,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( eventuality(U,V) % 116.74/116.79 => specific(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax27,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( thing(U,V) % 116.74/116.79 => singleton(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax28,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( eventuality(U,V) % 116.74/116.79 => thing(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax29,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( event(U,V) % 116.74/116.79 => eventuality(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax30,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( smoke(U,V) % 116.74/116.79 => event(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax31,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( existent(U,V) % 116.74/116.79 => ~ nonexistent(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax32,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( nonhuman(U,V) % 116.74/116.79 => ~ human(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax33,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( specific(U,V) % 116.74/116.79 => ~ general(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax34,axiom, % 116.74/116.79 ! [U,V] : % 116.74/116.79 ( unisex(U,V) % 116.74/116.79 => ~ male(U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax35,axiom, % 116.74/116.79 ! [U,V,W] : % 116.74/116.79 ( ( accessible_world(V,W) % 116.74/116.79 & jules_forename(V,U) ) % 116.74/116.79 => jules_forename(W,U) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax36,axiom, % 116.74/116.79 ! [U,V,W,X] : % 116.74/116.79 ( ( accessible_world(W,X) % 116.74/116.79 & of(W,U,V) ) % 116.74/116.79 => of(X,U,V) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax37,axiom, % 116.74/116.79 ! [U,V,W] : % 116.74/116.79 ( ( accessible_world(V,W) % 116.74/116.79 & vincent_forename(V,U) ) % 116.74/116.79 => vincent_forename(W,U) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax38,axiom, % 116.74/116.79 ! [U,V,W] : % 116.74/116.79 ( ( accessible_world(V,W) % 116.74/116.79 & relname(V,U) ) % 116.74/116.79 => relname(W,U) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax39,axiom, % 116.74/116.79 ! [U,V,W] : % 116.74/116.79 ( ( accessible_world(V,W) % 116.74/116.79 & forename(V,U) ) % 116.74/116.79 => forename(W,U) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax40,axiom, % 116.74/116.79 ! [U,V,W] : % 116.74/116.79 ( ( accessible_world(V,W) % 116.74/116.79 & male(V,U) ) % 116.74/116.79 => male(W,U) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax41,axiom, % 116.74/116.79 ! [U,V,W] : % 116.74/116.79 ( ( accessible_world(V,W) % 116.74/116.79 & animate(V,U) ) % 116.74/116.79 => animate(W,U) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax42,axiom, % 116.74/116.79 ! [U,V,W] : % 116.74/116.79 ( ( accessible_world(V,W) % 116.74/116.79 & human(V,U) ) % 116.74/116.79 => human(W,U) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax43,axiom, % 116.74/116.79 ! [U,V,W] : % 116.74/116.79 ( ( accessible_world(V,W) % 116.74/116.79 & living(V,U) ) % 116.74/116.79 => living(W,U) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax44,axiom, % 116.74/116.79 ! [U,V,W] : % 116.74/116.79 ( ( accessible_world(V,W) % 116.74/116.79 & impartial(V,U) ) % 116.74/116.79 => impartial(W,U) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax45,axiom, % 116.74/116.79 ! [U,V,W] : % 116.74/116.79 ( ( accessible_world(V,W) % 116.74/116.79 & existent(V,U) ) % 116.74/116.79 => existent(W,U) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax46,axiom, % 116.74/116.79 ! [U,V,W] : % 116.74/116.79 ( ( accessible_world(V,W) % 116.74/116.79 & entity(V,U) ) % 116.74/116.79 => entity(W,U) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax47,axiom, % 116.74/116.79 ! [U,V,W] : % 116.74/116.79 ( ( accessible_world(V,W) % 116.74/116.79 & organism(V,U) ) % 116.74/116.79 => organism(W,U) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax48,axiom, % 116.74/116.79 ! [U,V,W] : % 116.74/116.79 ( ( accessible_world(V,W) % 116.74/116.79 & human_person(V,U) ) % 116.74/116.79 => human_person(W,U) ) ). % 116.74/116.79 % 116.74/116.79 fof(ax49,axiom, % 116.74/116.79 ! [U,V,W] : % 116.74/116.79 ( ( accessible_world(V,W) % 116.74/116.80 & man(V,U) ) % 116.74/116.80 => man(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax50,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & state(V,U) ) % 116.74/116.80 => state(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax51,axiom, % 116.74/116.80 ! [U,V,W,X,Y] : % 116.74/116.80 ( ( accessible_world(X,Y) % 116.74/116.80 & be(X,U,V,W) ) % 116.74/116.80 => be(Y,U,V,W) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax52,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & general(V,U) ) % 116.74/116.80 => general(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax53,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & nonhuman(V,U) ) % 116.74/116.80 => nonhuman(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax54,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & abstraction(V,U) ) % 116.74/116.80 => abstraction(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax55,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & relation(V,U) ) % 116.74/116.80 => relation(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax56,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & proposition(V,U) ) % 116.74/116.80 => proposition(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax57,axiom, % 116.74/116.80 ! [U,V,W,X] : % 116.74/116.80 ( ( accessible_world(W,X) % 116.74/116.80 & theme(W,U,V) ) % 116.74/116.80 => theme(X,U,V) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax58,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & think_believe_consider(V,U) ) % 116.74/116.80 => think_believe_consider(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax59,axiom, % 116.74/116.80 ! [U,V,W,X] : % 116.74/116.80 ( ( accessible_world(W,X) % 116.74/116.80 & agent(W,U,V) ) % 116.74/116.80 => agent(X,U,V) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax60,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & present(V,U) ) % 116.74/116.80 => present(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax61,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & unisex(V,U) ) % 116.74/116.80 => unisex(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax62,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & nonexistent(V,U) ) % 116.74/116.80 => nonexistent(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax63,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & specific(V,U) ) % 116.74/116.80 => specific(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax64,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & singleton(V,U) ) % 116.74/116.80 => singleton(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax65,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & thing(V,U) ) % 116.74/116.80 => thing(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax66,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & eventuality(V,U) ) % 116.74/116.80 => eventuality(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax67,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & event(V,U) ) % 116.74/116.80 => event(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax68,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( accessible_world(V,W) % 116.74/116.80 & smoke(V,U) ) % 116.74/116.80 => smoke(W,U) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax69,axiom, % 116.74/116.80 ! [U,V,W] : % 116.74/116.80 ( ( entity(U,V) % 116.74/116.80 & forename(U,W) % 116.74/116.80 & of(U,W,V) ) % 116.74/116.80 => ~ ? [X] : % 116.74/116.80 ( forename(U,X) % 116.74/116.80 & X != W % 116.74/116.80 & of(U,X,V) ) ) ). % 116.74/116.80 % 116.74/116.80 fof(ax70,axiom, % 116.74/116.80 ! [U,V,W,X] : % 116.74/116.80 ( be(U,V,W,X) % 116.74/116.80 => W = X ) ). % 116.74/116.80 % 116.74/116.80 fof(ax71,axiom, % 116.74/116.80 ! [U,V,W,X,Y,Z] : % 116.74/116.80 ( ( think_believe_consider(U,V) % 116.74/116.80 & proposition(U,Y) % 116.74/116.80 & theme(U,V,Y) % 116.74/116.80 & agent(U,V,X) % 116.74/116.80 & think_believe_consider(U,W) % 116.74/116.80 & proposition(U,Z) % 116.74/116.80 & theme(U,W,Z) % 116.74/116.80 & agent(U,W,X) ) % 116.74/116.80 => Y = Z ) ). % 116.74/116.80 % 116.74/116.80 fof(co1,conjecture, % 116.74/116.80 ~ ( ? [U] : % 116.74/116.80 ( actual_world(U) % 116.74/116.80 & ? [V,W,X,Y,Z,X1,X2] : % 116.74/116.80 ( of(U,W,V) % 116.74/116.80 & man(U,V) % 116.74/116.80 & vincent_forename(U,W) % 116.74/116.80 & forename(U,W) % 116.74/116.80 & proposition(U,Y) % 116.74/116.80 & agent(U,X,V) % 116.74/116.80 & theme(U,X,Y) % 116.74/116.80 & event(U,X) % 116.74/116.80 & present(U,X) % 116.74/116.80 & think_believe_consider(U,X) % 116.74/116.80 & accessible_world(U,Y) % 116.74/116.80 & ! [X3] : % 116.74/116.80 ( man(Y,X3) % 116.74/116.80 => ? [X4] : % 116.74/116.80 ( event(Y,X4) % 116.74/116.80 & agent(Y,X4,X3) % 116.74/116.80 & present(Y,X4) % 116.74/116.80 & smoke(Y,X4) ) ) % 116.74/116.80 & of(U,Z,X1) % 116.74/116.80 & man(U,X1) % 116.74/116.80 & jules_forename(U,Z) % 116.74/116.80 & forename(U,Z) % 116.74/116.80 & man(U,X1) % 116.74/116.80 & state(U,X2) % 116.74/116.80 & be(U,X2,X1,X1) ) ) % 116.74/116.80 & ~ ? [X5] : % 116.74/116.80 ( actual_world(X5) % 116.74/116.80 & ? [X6,X7,X8,V,W,X,Y,Z,X1,X2,X9,X10] : % 116.74/116.80 ( of(X5,X7,X6) % 116.74/116.80 & man(X5,X6) % 116.74/116.80 & jules_forename(X5,X7) % 116.74/116.80 & forename(X5,X7) % 116.74/116.80 & of(X5,X8,V) % 116.74/116.80 & vincent_forename(X5,X8) % 116.74/116.80 & forename(X5,X8) % 116.74/116.80 & of(X5,W,V) % 116.74/116.80 & man(X5,V) % 116.74/116.80 & vincent_forename(X5,W) % 116.74/116.80 & forename(X5,W) % 116.74/116.80 & proposition(X5,Y) % 116.74/116.80 & agent(X5,X,V) % 116.74/116.80 & theme(X5,X,Y) % 116.74/116.80 & event(X5,X) % 116.74/116.80 & present(X5,X) % 116.74/116.80 & think_believe_consider(X5,X) % 116.74/116.80 & accessible_world(X5,Y) % 116.74/116.80 & ! [X3] : % 116.74/116.80 ( man(Y,X3) % 116.74/116.80 => ? [X4] : % 116.74/116.80 ( event(Y,X4) % 116.74/116.80 & agent(Y,X4,X3) % 116.74/116.80 & present(Y,X4) % 116.74/116.80 & smoke(Y,X4) ) ) % 116.74/116.80 & of(X5,Z,X1) % 116.74/116.80 & man(X5,X1) % 116.74/116.80 & jules_forename(X5,Z) % 116.74/116.80 & forename(X5,Z) % 116.74/116.80 & man(X5,X1) % 116.74/116.80 & state(X5,X2) % 116.74/116.80 & be(X5,X2,X1,X1) % 116.74/116.80 & proposition(X5,X10) % 116.74/116.80 & agent(X5,X9,V) % 116.74/116.80 & theme(X5,X9,X10) % 116.74/116.80 & event(X5,X9) % 116.74/116.80 & present(X5,X9) % 116.74/116.80 & think_believe_consider(X5,X9) % 116.74/116.80 & accessible_world(X5,X10) % 116.74/116.80 & ? [X11] : % 116.74/116.80 ( event(X10,X11) % 116.74/116.80 & agent(X10,X11,X6) % 116.74/116.80 & present(X10,X11) % 116.74/116.80 & smoke(X10,X11) ) ) ) ) ). % 116.74/116.80 % 116.74/116.80 %-------------------------------------------------------------------------- % 116.74/116.80 %------------------------------------------- % 116.74/116.80 % Proof found % 116.74/116.80 % SZS status Theorem for theBenchmark % 116.74/116.80 % SZS output start Proof % 116.74/116.80 %ClaNum:189(EqnAxiom:93) % 116.74/116.80 %VarNum:600(SingletonVarNum:222) % 116.74/116.80 %MaxLitNum:40 % 116.74/116.80 %MaxfuncDepth:1 % 116.74/116.80 %SharedTerms:26 % 116.74/116.80 %goalClause: 94 95 96 97 98 99 101 102 103 104 105 106 107 108 109 110 111 112 143 144 145 180 188 189 % 116.74/116.80 %singleGoalClaCount:18 % 116.74/116.80 [94]P1(a1) % 116.74/116.80 [95]P4(a1,a3) % 116.74/116.80 [96]P5(a1,a4) % 116.74/116.80 [97]P5(a1,a3) % 116.74/116.80 [98]P17(a1,a4) % 116.74/116.80 [99]P18(a1,a5) % 116.74/116.80 [101]P18(a1,a8) % 116.74/116.80 [102]P21(a1,a9) % 116.74/116.80 [103]P6(a1,a6) % 116.74/116.80 [104]P22(a1,a7) % 116.74/116.80 [105]P2(a1,a7) % 116.74/116.80 [106]P33(a1,a6) % 116.74/116.80 [107]P23(a1,a6) % 116.74/116.80 [108]P24(a1,a4,a5) % 116.74/116.80 [109]P24(a1,a3,a8) % 116.74/116.80 [110]P34(a1,a6,a7) % 116.74/116.80 [111]P7(a1,a6,a5) % 116.74/116.80 [112]P8(a1,a9,a8,a8) % 116.74/116.80 [143]~P18(a7,x1431)+P6(a7,f10(x1431)) % 116.74/116.80 [144]~P18(a7,x1441)+P31(a7,f10(x1441)) % 116.74/116.80 [145]~P18(a7,x1451)+P23(a7,f10(x1451)) % 116.74/116.80 [180]~P18(a7,x1801)+P7(a7,f10(x1801),x1801) % 116.74/116.80 [113]~P4(x1131,x1132)+P5(x1131,x1132) % 116.74/116.80 [114]~P17(x1141,x1142)+P5(x1141,x1142) % 116.74/116.80 [115]~P5(x1151,x1152)+P28(x1151,x1152) % 116.74/116.80 [116]~P28(x1161,x1162)+P29(x1161,x1162) % 116.74/116.80 [117]~P22(x1171,x1172)+P29(x1171,x1172) % 116.74/116.80 [118]~P18(x1181,x1182)+P19(x1181,x1182) % 116.74/116.80 [119]~P18(x1191,x1192)+P13(x1191,x1192) % 116.74/116.80 [120]~P13(x1201,x1202)+P9(x1201,x1202) % 116.74/116.80 [121]~P13(x1211,x1212)+P14(x1211,x1212) % 116.74/116.80 [122]~P13(x1221,x1222)+P27(x1221,x1222) % 116.74/116.80 [123]~P27(x1231,x1232)+P20(x1231,x1232) % 116.74/116.80 [124]~P27(x1241,x1242)+P16(x1241,x1242) % 116.74/116.80 [125]~P27(x1251,x1252)+P10(x1251,x1252) % 116.74/116.80 [126]~P10(x1261,x1262)+P11(x1261,x1262) % 116.74/116.80 [127]~P10(x1271,x1272)+P30(x1271,x1272) % 116.74/116.80 [128]~P12(x1281,x1282)+P30(x1281,x1282) % 116.74/116.80 [129]~P10(x1291,x1292)+P35(x1291,x1292) % 116.74/116.80 [130]~P12(x1301,x1302)+P35(x1301,x1302) % 116.74/116.80 [131]~P3(x1311,x1312)+P35(x1311,x1312) % 116.74/116.80 [132]~P21(x1321,x1322)+P6(x1321,x1322) % 116.74/116.80 [133]~P31(x1331,x1332)+P6(x1331,x1332) % 116.74/116.80 [134]~P21(x1341,x1342)+P12(x1341,x1342) % 116.74/116.80 [135]~P6(x1351,x1352)+P12(x1351,x1352) % 116.74/116.80 [136]~P29(x1361,x1362)+P3(x1361,x1362) % 116.74/116.80 [137]~P12(x1371,x1372)+P36(x1371,x1372) % 116.74/116.80 [138]~P3(x1381,x1382)+P36(x1381,x1382) % 116.74/116.80 [139]~P3(x1391,x1392)+P15(x1391,x1392) % 116.74/116.80 [140]~P3(x1401,x1402)+P25(x1401,x1402) % 116.74/116.80 [141]~P12(x1411,x1412)+P26(x1411,x1412) % 116.74/116.80 [142]~P35(x1421,x1422)+P32(x1421,x1422) % 116.74/116.80 [146]~P36(x1461,x1462)+~P19(x1461,x1462) % 116.74/116.80 [147]~P25(x1471,x1472)+~P14(x1471,x1472) % 116.74/116.80 [148]~P26(x1481,x1482)+~P11(x1481,x1482) % 116.74/116.80 [149]~P15(x1491,x1492)+~P30(x1491,x1492) % 116.74/116.80 [185]E(x1851,x1852)+~P8(x1853,x1854,x1851,x1852) % 116.74/116.80 [150]~P2(x1503,x1501)+P4(x1501,x1502)+~P4(x1503,x1502) % 116.74/116.80 [151]~P2(x1513,x1511)+P5(x1511,x1512)+~P5(x1513,x1512) % 116.74/116.80 [152]~P2(x1523,x1521)+P17(x1521,x1522)+~P17(x1523,x1522) % 116.74/116.80 [153]~P2(x1533,x1531)+P28(x1531,x1532)+~P28(x1533,x1532) % 116.74/116.80 [154]~P2(x1543,x1541)+P29(x1541,x1542)+~P29(x1543,x1542) % 116.74/116.80 [155]~P2(x1553,x1551)+P18(x1551,x1552)+~P18(x1553,x1552) % 116.74/116.80 [156]~P2(x1563,x1561)+P19(x1561,x1562)+~P19(x1563,x1562) % 116.74/116.80 [157]~P2(x1573,x1571)+P13(x1571,x1572)+~P13(x1573,x1572) % 116.74/116.80 [158]~P2(x1583,x1581)+P9(x1581,x1582)+~P9(x1583,x1582) % 116.74/116.80 [159]~P2(x1593,x1591)+P14(x1591,x1592)+~P14(x1593,x1592) % 116.74/116.80 [160]~P2(x1603,x1601)+P27(x1601,x1602)+~P27(x1603,x1602) % 116.74/116.80 [161]~P2(x1613,x1611)+P20(x1611,x1612)+~P20(x1613,x1612) % 116.74/116.80 [162]~P2(x1623,x1621)+P16(x1621,x1622)+~P16(x1623,x1622) % 116.74/116.80 [163]~P2(x1633,x1631)+P10(x1631,x1632)+~P10(x1633,x1632) % 116.74/116.80 [164]~P2(x1643,x1641)+P11(x1641,x1642)+~P11(x1643,x1642) % 116.74/116.80 [165]~P2(x1653,x1651)+P30(x1651,x1652)+~P30(x1653,x1652) % 116.74/116.80 [166]~P2(x1663,x1661)+P35(x1661,x1662)+~P35(x1663,x1662) % 116.74/116.80 [167]~P2(x1673,x1671)+P21(x1671,x1672)+~P21(x1673,x1672) % 116.74/116.80 [168]~P2(x1683,x1681)+P6(x1681,x1682)+~P6(x1683,x1682) % 116.74/116.80 [169]~P2(x1693,x1691)+P12(x1691,x1692)+~P12(x1693,x1692) % 116.74/116.80 [170]~P2(x1703,x1701)+P3(x1701,x1702)+~P3(x1703,x1702) % 116.74/116.80 [171]~P2(x1713,x1711)+P36(x1711,x1712)+~P36(x1713,x1712) % 116.74/116.80 [172]~P2(x1723,x1721)+P15(x1721,x1722)+~P15(x1723,x1722) % 116.74/116.80 [173]~P2(x1733,x1731)+P25(x1731,x1732)+~P25(x1733,x1732) % 116.74/116.80 [174]~P2(x1743,x1741)+P22(x1741,x1742)+~P22(x1743,x1742) % 116.74/116.80 [175]~P2(x1753,x1751)+P26(x1751,x1752)+~P26(x1753,x1752) % 116.74/116.80 [176]~P2(x1763,x1761)+P32(x1761,x1762)+~P32(x1763,x1762) % 116.74/116.80 [177]~P2(x1773,x1771)+P31(x1771,x1772)+~P31(x1773,x1772) % 116.74/116.80 [178]~P33(x1783,x1782)+P33(x1781,x1782)+~P2(x1783,x1781) % 116.74/116.80 [179]~P23(x1793,x1792)+P23(x1791,x1792)+~P2(x1793,x1791) % 116.74/116.80 [181]~P24(x1814,x1812,x1813)+P24(x1811,x1812,x1813)+~P2(x1814,x1811) % 116.74/116.80 [182]~P34(x1824,x1822,x1823)+P34(x1821,x1822,x1823)+~P2(x1824,x1821) % 116.74/116.80 [183]~P7(x1834,x1832,x1833)+P7(x1831,x1832,x1833)+~P2(x1834,x1831) % 116.74/116.80 [187]~P8(x1875,x1872,x1873,x1874)+P8(x1871,x1872,x1873,x1874)+~P2(x1875,x1871) % 116.74/116.80 [184]~P5(x1843,x1841)+~P24(x1843,x1842,x1844)+~P24(x1843,x1841,x1844)+E(x1841,x1842)+~P5(x1843,x1842)+~P10(x1843,x1844) % 116.74/116.80 [186]~P22(x1863,x1861)+~P34(x1863,x1864,x1862)+~P34(x1863,x1865,x1861)+~P7(x1863,x1865,x1866)+E(x1861,x1862)+~P22(x1863,x1862)+~P33(x1863,x1864)+~P7(x1863,x1864,x1866)+~P33(x1863,x1865) % 116.74/116.80 [188]P18(x1881,f2(x1882,x1883,x1884,x1885,x1886,x1887,x1888,x1881,x1889,x18810,x18811,x18812,x18813))+~P1(x1882)+~P4(x1882,x1889)+~P4(x1882,x1884)+~P5(x1882,x1889)+~P5(x1882,x1887)+~P5(x1882,x1885)+~P5(x1882,x1884)+~P17(x1882,x1887)+~P17(x1882,x1885)+~P18(x1882,x18810)+~P18(x1882,x1886)+~P18(x1882,x1883)+~P21(x1882,x18811)+~P6(x18813,x18814)+~P6(x1882,x18812)+~P6(x1882,x1888)+~P22(x1882,x18813)+~P22(x1882,x1881)+~P31(x18813,x18814)+~P2(x1882,x18813)+~P2(x1882,x1881)+~P33(x1882,x18812)+~P33(x1882,x1888)+~P23(x18813,x18814)+~P23(x1882,x18812)+~P23(x1882,x1888)+~P24(x1882,x1889,x18810)+~P24(x1882,x1887,x1886)+~P24(x1882,x1885,x1886)+~P24(x1882,x1884,x1883)+~P34(x1882,x18812,x18813)+~P34(x1882,x1888,x1881)+~P7(x18813,x18814,x1883)+~P7(x1882,x18812,x1886)+~P7(x1882,x1888,x1886)+~P8(x1882,x18811,x18810,x18810) % 116.74/116.80 [189]~P1(x1891)+~P4(x1891,x1892)+~P4(x1891,x1893)+~P5(x1891,x1892)+~P5(x1891,x1894)+~P5(x1891,x1895)+~P5(x1891,x1893)+~P17(x1891,x1894)+~P17(x1891,x1895)+~P18(x1891,x1896)+~P18(x1891,x1897)+~P18(x1891,x1898)+~P21(x1891,x1899)+~P6(x18910,x18911)+~P6(x1891,x18912)+~P6(x1891,x18913)+~P6(x18914,x18915)+~P22(x1891,x18910)+~P22(x1891,x18914)+~P31(x18910,x18911)+~P31(x18914,x18915)+~P2(x1891,x18910)+~P2(x1891,x18914)+~P33(x1891,x18912)+~P33(x1891,x18913)+~P23(x18910,x18911)+~P23(x1891,x18912)+~P23(x1891,x18913)+~P23(x18914,x18915)+~P24(x1891,x1892,x1896)+~P24(x1891,x1894,x1897)+~P24(x1891,x1895,x1897)+~P24(x1891,x1893,x1898)+~P34(x1891,x18912,x18910)+~P34(x1891,x18913,x18914)+~P7(x18910,x18911,x1898)+~P7(x1891,x18912,x1897)+~P7(x1891,x18913,x1897)+~P8(x1891,x1899,x1896,x1896)+~P7(x18914,x18915,f2(x1891,x1898,x1893,x1895,x1897,x1894,x18913,x18914,x1892,x1896,x1899,x18912,x18910)) % 116.74/116.80 %EqnAxiom % 116.74/116.80 [1]E(x11,x11) % 116.74/116.80 [2]E(x22,x21)+~E(x21,x22) % 116.74/116.80 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.74/116.80 [4]~E(x41,x42)+E(f10(x41),f10(x42)) % 116.74/116.80 [5]~E(x51,x52)+E(f2(x51,x53,x54,x55,x56,x57,x58,x59,x510,x511,x512,x513,x514),f2(x52,x53,x54,x55,x56,x57,x58,x59,x510,x511,x512,x513,x514)) % 116.74/116.80 [6]~E(x61,x62)+E(f2(x63,x61,x64,x65,x66,x67,x68,x69,x610,x611,x612,x613,x614),f2(x63,x62,x64,x65,x66,x67,x68,x69,x610,x611,x612,x613,x614)) % 116.74/116.80 [7]~E(x71,x72)+E(f2(x73,x74,x71,x75,x76,x77,x78,x79,x710,x711,x712,x713,x714),f2(x73,x74,x72,x75,x76,x77,x78,x79,x710,x711,x712,x713,x714)) % 116.74/116.80 [8]~E(x81,x82)+E(f2(x83,x84,x85,x81,x86,x87,x88,x89,x810,x811,x812,x813,x814),f2(x83,x84,x85,x82,x86,x87,x88,x89,x810,x811,x812,x813,x814)) % 116.74/116.80 [9]~E(x91,x92)+E(f2(x93,x94,x95,x96,x91,x97,x98,x99,x910,x911,x912,x913,x914),f2(x93,x94,x95,x96,x92,x97,x98,x99,x910,x911,x912,x913,x914)) % 116.74/116.80 [10]~E(x101,x102)+E(f2(x103,x104,x105,x106,x107,x101,x108,x109,x1010,x1011,x1012,x1013,x1014),f2(x103,x104,x105,x106,x107,x102,x108,x109,x1010,x1011,x1012,x1013,x1014)) % 116.74/116.80 [11]~E(x111,x112)+E(f2(x113,x114,x115,x116,x117,x118,x111,x119,x1110,x1111,x1112,x1113,x1114),f2(x113,x114,x115,x116,x117,x118,x112,x119,x1110,x1111,x1112,x1113,x1114)) % 116.74/116.80 [12]~E(x121,x122)+E(f2(x123,x124,x125,x126,x127,x128,x129,x121,x1210,x1211,x1212,x1213,x1214),f2(x123,x124,x125,x126,x127,x128,x129,x122,x1210,x1211,x1212,x1213,x1214)) % 116.74/116.80 [13]~E(x131,x132)+E(f2(x133,x134,x135,x136,x137,x138,x139,x1310,x131,x1311,x1312,x1313,x1314),f2(x133,x134,x135,x136,x137,x138,x139,x1310,x132,x1311,x1312,x1313,x1314)) % 116.74/116.80 [14]~E(x141,x142)+E(f2(x143,x144,x145,x146,x147,x148,x149,x1410,x1411,x141,x1412,x1413,x1414),f2(x143,x144,x145,x146,x147,x148,x149,x1410,x1411,x142,x1412,x1413,x1414)) % 116.74/116.80 [15]~E(x151,x152)+E(f2(x153,x154,x155,x156,x157,x158,x159,x1510,x1511,x1512,x151,x1513,x1514),f2(x153,x154,x155,x156,x157,x158,x159,x1510,x1511,x1512,x152,x1513,x1514)) % 116.74/116.80 [16]~E(x161,x162)+E(f2(x163,x164,x165,x166,x167,x168,x169,x1610,x1611,x1612,x1613,x161,x1614),f2(x163,x164,x165,x166,x167,x168,x169,x1610,x1611,x1612,x1613,x162,x1614)) % 116.74/116.80 [17]~E(x171,x172)+E(f2(x173,x174,x175,x176,x177,x178,x179,x1710,x1711,x1712,x1713,x1714,x171),f2(x173,x174,x175,x176,x177,x178,x179,x1710,x1711,x1712,x1713,x1714,x172)) % 116.74/116.80 [18]~P1(x181)+P1(x182)+~E(x181,x182) % 116.74/116.80 [19]P4(x192,x193)+~E(x191,x192)+~P4(x191,x193) % 116.74/116.80 [20]P4(x203,x202)+~E(x201,x202)+~P4(x203,x201) % 116.74/116.80 [21]P5(x212,x213)+~E(x211,x212)+~P5(x211,x213) % 116.74/116.80 [22]P5(x223,x222)+~E(x221,x222)+~P5(x223,x221) % 116.74/116.80 [23]P24(x232,x233,x234)+~E(x231,x232)+~P24(x231,x233,x234) % 116.74/116.80 [24]P24(x243,x242,x244)+~E(x241,x242)+~P24(x243,x241,x244) % 116.74/116.80 [25]P24(x253,x254,x252)+~E(x251,x252)+~P24(x253,x254,x251) % 116.74/116.80 [26]P17(x262,x263)+~E(x261,x262)+~P17(x261,x263) % 116.74/116.80 [27]P17(x273,x272)+~E(x271,x272)+~P17(x273,x271) % 116.74/116.80 [28]P18(x282,x283)+~E(x281,x282)+~P18(x281,x283) % 116.74/116.80 [29]P18(x293,x292)+~E(x291,x292)+~P18(x293,x291) % 116.74/116.80 [30]P34(x302,x303,x304)+~E(x301,x302)+~P34(x301,x303,x304) % 116.74/116.80 [31]P34(x313,x312,x314)+~E(x311,x312)+~P34(x313,x311,x314) % 116.74/116.80 [32]P34(x323,x324,x322)+~E(x321,x322)+~P34(x323,x324,x321) % 116.74/116.80 [33]P22(x332,x333)+~E(x331,x332)+~P22(x331,x333) % 116.74/116.81 [34]P22(x343,x342)+~E(x341,x342)+~P22(x343,x341) % 116.74/116.81 [35]P21(x352,x353)+~E(x351,x352)+~P21(x351,x353) % 116.74/116.81 [36]P21(x363,x362)+~E(x361,x362)+~P21(x363,x361) % 116.74/116.81 [37]P6(x372,x373)+~E(x371,x372)+~P6(x371,x373) % 116.74/116.81 [38]P6(x383,x382)+~E(x381,x382)+~P6(x383,x381) % 116.74/116.81 [39]P31(x392,x393)+~E(x391,x392)+~P31(x391,x393) % 116.74/116.81 [40]P31(x403,x402)+~E(x401,x402)+~P31(x403,x401) % 116.74/116.81 [41]P2(x412,x413)+~E(x411,x412)+~P2(x411,x413) % 116.74/116.81 [42]P2(x423,x422)+~E(x421,x422)+~P2(x423,x421) % 116.74/116.81 [43]P33(x432,x433)+~E(x431,x432)+~P33(x431,x433) % 116.74/116.81 [44]P33(x443,x442)+~E(x441,x442)+~P33(x443,x441) % 116.74/116.81 [45]P23(x452,x453)+~E(x451,x452)+~P23(x451,x453) % 116.74/116.81 [46]P23(x463,x462)+~E(x461,x462)+~P23(x463,x461) % 116.74/116.81 [47]P7(x472,x473,x474)+~E(x471,x472)+~P7(x471,x473,x474) % 116.74/116.81 [48]P7(x483,x482,x484)+~E(x481,x482)+~P7(x483,x481,x484) % 116.74/116.81 [49]P7(x493,x494,x492)+~E(x491,x492)+~P7(x493,x494,x491) % 116.74/116.81 [50]P8(x502,x503,x504,x505)+~E(x501,x502)+~P8(x501,x503,x504,x505) % 116.74/116.81 [51]P8(x513,x512,x514,x515)+~E(x511,x512)+~P8(x513,x511,x514,x515) % 116.74/116.81 [52]P8(x523,x524,x522,x525)+~E(x521,x522)+~P8(x523,x524,x521,x525) % 116.74/116.81 [53]P8(x533,x534,x535,x532)+~E(x531,x532)+~P8(x533,x534,x535,x531) % 116.74/116.81 [54]P20(x542,x543)+~E(x541,x542)+~P20(x541,x543) % 116.74/116.81 [55]P20(x553,x552)+~E(x551,x552)+~P20(x553,x551) % 116.74/116.81 [56]P26(x562,x563)+~E(x561,x562)+~P26(x561,x563) % 116.74/116.81 [57]P26(x573,x572)+~E(x571,x572)+~P26(x573,x571) % 116.74/116.81 [58]P13(x582,x583)+~E(x581,x582)+~P13(x581,x583) % 116.74/116.81 [59]P13(x593,x592)+~E(x591,x592)+~P13(x593,x591) % 116.74/116.81 [60]P29(x602,x603)+~E(x601,x602)+~P29(x601,x603) % 116.74/116.81 [61]P29(x613,x612)+~E(x611,x612)+~P29(x613,x611) % 116.74/116.81 [62]P15(x622,x623)+~E(x621,x622)+~P15(x621,x623) % 116.74/116.81 [63]P15(x633,x632)+~E(x631,x632)+~P15(x633,x631) % 116.74/116.81 [64]P3(x642,x643)+~E(x641,x642)+~P3(x641,x643) % 116.74/116.81 [65]P3(x653,x652)+~E(x651,x652)+~P3(x653,x651) % 116.74/116.81 [66]P27(x662,x663)+~E(x661,x662)+~P27(x661,x663) % 116.74/116.81 [67]P27(x673,x672)+~E(x671,x672)+~P27(x673,x671) % 116.74/116.81 [68]P28(x682,x683)+~E(x681,x682)+~P28(x681,x683) % 116.74/116.81 [69]P28(x693,x692)+~E(x691,x692)+~P28(x693,x691) % 116.74/116.81 [70]P11(x702,x703)+~E(x701,x702)+~P11(x701,x703) % 116.74/116.81 [71]P11(x713,x712)+~E(x711,x712)+~P11(x713,x711) % 116.74/116.81 [72]P19(x722,x723)+~E(x721,x722)+~P19(x721,x723) % 116.74/116.81 [73]P19(x733,x732)+~E(x731,x732)+~P19(x733,x731) % 116.74/116.81 [74]P10(x742,x743)+~E(x741,x742)+~P10(x741,x743) % 116.74/116.81 [75]P10(x753,x752)+~E(x751,x752)+~P10(x753,x751) % 116.74/116.81 [76]P12(x762,x763)+~E(x761,x762)+~P12(x761,x763) % 116.74/116.81 [77]P12(x773,x772)+~E(x771,x772)+~P12(x773,x771) % 116.74/116.81 [78]P35(x782,x783)+~E(x781,x782)+~P35(x781,x783) % 116.74/116.81 [79]P35(x793,x792)+~E(x791,x792)+~P35(x793,x791) % 116.74/116.81 [80]P36(x802,x803)+~E(x801,x802)+~P36(x801,x803) % 116.74/116.81 [81]P36(x813,x812)+~E(x811,x812)+~P36(x813,x811) % 116.74/116.81 [82]P25(x822,x823)+~E(x821,x822)+~P25(x821,x823) % 116.74/116.81 [83]P25(x833,x832)+~E(x831,x832)+~P25(x833,x831) % 116.74/116.81 [84]P32(x842,x843)+~E(x841,x842)+~P32(x841,x843) % 116.74/116.81 [85]P32(x853,x852)+~E(x851,x852)+~P32(x853,x851) % 116.74/116.81 [86]P14(x862,x863)+~E(x861,x862)+~P14(x861,x863) % 116.74/116.81 [87]P14(x873,x872)+~E(x871,x872)+~P14(x873,x871) % 116.74/116.81 [88]P9(x882,x883)+~E(x881,x882)+~P9(x881,x883) % 116.74/116.81 [89]P9(x893,x892)+~E(x891,x892)+~P9(x893,x891) % 116.74/116.81 [90]P30(x902,x903)+~E(x901,x902)+~P30(x901,x903) % 116.74/116.81 [91]P30(x913,x912)+~E(x911,x912)+~P30(x913,x911) % 116.74/116.81 [92]P16(x922,x923)+~E(x921,x922)+~P16(x921,x923) % 116.74/116.81 [93]P16(x933,x932)+~E(x931,x932)+~P16(x933,x931) % 116.74/116.81 % 116.74/116.81 %------------------------------------------- % 116.74/116.81 cnf(192,plain, % 116.74/116.81 (P5(a7,a4)), % 116.74/116.81 inference(scs_inference,[],[95,96,105,150,151])). % 116.74/116.81 cnf(196,plain, % 116.74/116.81 (P18(a7,a5)), % 116.74/116.81 inference(scs_inference,[],[95,96,98,99,105,150,151,152,155])). % 116.74/116.81 cnf(200,plain, % 116.74/116.81 (P6(a7,a6)), % 116.74/116.81 inference(scs_inference,[],[95,96,98,99,102,103,105,150,151,152,155,167,168])). % 116.74/116.81 cnf(202,plain, % 116.74/116.81 (P22(a7,a7)), % 116.74/116.81 inference(scs_inference,[],[95,96,98,99,102,103,104,105,150,151,152,155,167,168,174])). % 116.74/116.81 cnf(230,plain, % 116.74/116.81 (P18(a7,a8)), % 116.74/116.81 inference(scs_inference,[],[101,109,105,181,155])). % 116.74/116.81 cnf(342,plain, % 116.74/116.81 (P6(a7,x3421)+~E(a6,x3421)), % 116.74/116.81 inference(scs_inference,[],[200,38])). % 116.74/116.81 cnf(420,plain, % 116.74/116.81 (P28(a1,a3)), % 116.74/116.81 inference(scs_inference,[],[95,113,115])). % 116.74/116.81 cnf(421,plain, % 116.74/116.81 (P28(a7,a3)), % 116.74/116.81 inference(scs_inference,[],[105,420,153])). % 116.74/116.81 cnf(424,plain, % 116.74/116.81 (P28(a1,x4241)+~E(a3,x4241)), % 116.74/116.81 inference(scs_inference,[],[105,420,153,68,69])). % 116.74/116.81 cnf(450,plain, % 116.74/116.81 (P28(a1,a4)), % 116.74/116.81 inference(scs_inference,[],[98,114,115])). % 116.74/116.81 cnf(451,plain, % 116.74/116.81 (P28(a7,a4)), % 116.74/116.81 inference(scs_inference,[],[105,450,153])). % 116.74/116.81 cnf(480,plain, % 116.74/116.81 (P3(a7,a3)), % 116.74/116.81 inference(scs_inference,[],[421,116,136])). % 116.74/116.81 cnf(503,plain, % 116.74/116.81 (P3(a1,a7)), % 116.74/116.81 inference(scs_inference,[],[104,117,136])). % 116.74/116.81 cnf(504,plain, % 116.74/116.81 (P3(a7,a7)), % 116.74/116.81 inference(scs_inference,[],[105,503,170])). % 116.74/116.81 cnf(506,plain, % 116.74/116.81 (P3(a1,x5061)+~E(a7,x5061)), % 116.74/116.81 inference(scs_inference,[],[105,503,170,65])). % 116.74/116.81 cnf(638,plain, % 116.74/116.81 (~P13(x6381,x6382)+~P25(x6381,x6382)), % 116.74/116.81 inference(scs_inference,[],[121,147])). % 116.74/116.81 cnf(686,plain, % 116.74/116.81 (P11(x6861,x6862)+~P27(x6861,x6862)), % 116.74/116.81 inference(scs_inference,[],[125,126])). % 116.74/116.81 cnf(702,plain, % 116.74/116.81 (~P10(x7021,x7022)+~P15(x7021,x7022)), % 116.74/116.81 inference(scs_inference,[],[127,149])). % 116.74/116.81 cnf(718,plain, % 116.74/116.81 (~P12(x7181,x7182)+~P15(x7181,x7182)), % 116.74/116.81 inference(scs_inference,[],[128,149])). % 116.74/116.81 cnf(734,plain, % 116.74/116.81 (P32(x7341,x7342)+~P10(x7341,x7342)), % 116.74/116.81 inference(scs_inference,[],[129,142])). % 116.74/116.81 cnf(750,plain, % 116.74/116.81 (P32(x7501,x7502)+~P12(x7501,x7502)), % 116.74/116.81 inference(scs_inference,[],[130,142])). % 116.74/116.81 cnf(789,plain, % 116.74/116.81 (P12(a1,a9)), % 116.74/116.81 inference(scs_inference,[],[102,132,135])). % 116.74/116.81 cnf(792,plain, % 116.74/116.81 (P12(a7,a9)), % 116.74/116.81 inference(scs_inference,[],[105,789,750,169])). % 116.74/116.81 cnf(832,plain, % 116.74/116.81 (~P10(a7,a7)), % 116.74/116.81 inference(scs_inference,[],[504,139,702])). % 116.74/116.81 cnf(833,plain, % 116.74/116.81 (~P27(a7,a7)), % 116.74/116.81 inference(scs_inference,[],[832,125])). % 116.74/116.81 cnf(835,plain, % 116.74/116.81 (~P13(a7,a7)), % 116.74/116.81 inference(scs_inference,[],[832,125,122])). % 116.74/116.81 cnf(876,plain, % 116.74/116.81 (~P11(a7,a9)), % 116.74/116.81 inference(scs_inference,[],[792,141,148])). % 116.74/116.81 cnf(1129,plain, % 116.74/116.81 (~P25(a1,x11291)+~P13(a7,x11291)), % 116.74/116.81 inference(scs_inference,[],[105,638,173])). % 116.74/116.81 cnf(1215,plain, % 116.74/116.81 (~P3(a7,a9)), % 116.74/116.81 inference(scs_inference,[],[792,718,139])). % 116.74/116.81 cnf(1216,plain, % 116.74/116.81 (~P29(a7,a9)), % 116.74/116.81 inference(scs_inference,[],[1215,136])). % 116.74/116.81 cnf(1224,plain, % 116.74/116.81 (~E(a4,a9)), % 116.74/116.81 inference(scs_inference,[],[192,1215,136,117,116,115,22])). % 116.74/116.81 cnf(1227,plain, % 116.74/116.81 (~P4(a7,a9)), % 116.74/116.81 inference(scs_inference,[],[202,192,421,1215,136,117,116,115,22,69,34,113])). % 116.74/116.81 cnf(1229,plain, % 116.74/116.81 (~P17(a7,a9)), % 116.74/116.81 inference(scs_inference,[],[202,192,421,1215,136,117,116,115,22,69,34,113,114])). % 116.74/116.81 cnf(1254,plain, % 116.74/116.81 (P32(x12541,x12542)+~P27(x12541,x12542)), % 116.74/116.81 inference(scs_inference,[],[734,125])). % 116.74/116.81 cnf(1479,plain, % 116.74/116.81 (P32(x14791,x14792)+~P13(x14791,x14792)), % 116.74/116.81 inference(scs_inference,[],[1254,122])). % 116.74/116.81 cnf(1750,plain, % 116.74/116.81 (P23(a7,f10(a5))), % 116.74/116.81 inference(scs_inference,[],[99,105,145,155])). % 116.74/116.81 cnf(1883,plain, % 116.74/116.81 (P7(a7,f10(a8),a8)), % 116.74/116.81 inference(scs_inference,[],[101,105,180,155])). % 116.74/116.81 cnf(1885,plain, % 116.74/116.81 (P7(a7,x18851,a8)+~E(f10(a8),x18851)), % 116.74/116.81 inference(scs_inference,[],[1883,47,48])). % 116.74/116.81 cnf(2819,plain, % 116.74/116.81 (P31(x28191,f10(a8))+~E(a7,x28191)), % 116.74/116.81 inference(scs_inference,[],[230,39,144])). % 116.74/116.81 cnf(2820,plain, % 116.74/116.81 (P31(a7,f10(a8))), % 116.74/116.81 inference(equality_inference,[],[2819])). % 116.74/116.81 cnf(3167,plain, % 116.74/116.81 (~P26(a1,x31671)+P26(x31672,x31671)+~E(a7,x31672)), % 116.74/116.81 inference(scs_inference,[],[105,56,175])). % 116.74/116.81 cnf(3168,plain, % 116.74/116.81 (P26(a7,x31681)+~P26(a1,x31681)), % 116.74/116.81 inference(equality_inference,[],[3167])). % 116.74/116.81 cnf(3184,plain, % 116.74/116.81 (P26(a7,a9)), % 116.74/116.81 inference(scs_inference,[],[789,3168,141])). % 116.74/116.81 cnf(3188,plain, % 116.74/116.81 (P26(a7,x31881)+~E(a9,x31881)), % 116.74/116.81 inference(scs_inference,[],[3184,175,56,57])). % 116.74/116.81 cnf(3240,plain, % 116.74/116.81 (~P13(a1,x32401)+~E(x32401,a7)), % 116.74/116.81 inference(scs_inference,[],[835,105,59,157])). % 116.74/116.81 cnf(3241,plain, % 116.74/116.81 (~P13(a1,a7)), % 116.74/116.81 inference(equality_inference,[],[3240])). % 116.74/116.81 cnf(3324,plain, % 116.74/116.81 (~P15(a1,x33241)+P15(x33242,x33241)+~E(a7,x33242)), % 116.74/116.81 inference(scs_inference,[],[105,62,172])). % 116.74/116.81 cnf(3325,plain, % 116.74/116.81 (P15(a7,x33251)+~P15(a1,x33251)), % 116.74/116.81 inference(equality_inference,[],[3324])). % 116.74/116.81 cnf(3341,plain, % 116.74/116.81 (P15(a7,a7)), % 116.74/116.81 inference(scs_inference,[],[503,3325,139])). % 116.74/116.81 cnf(3344,plain, % 116.74/116.81 (~P21(a7,a7)), % 116.74/116.81 inference(scs_inference,[],[3341,718,134])). % 116.74/116.81 cnf(3348,plain, % 116.74/116.81 (~P31(a7,a7)), % 116.74/116.81 inference(scs_inference,[],[3341,718,134,135,133])). % 116.74/116.81 cnf(3933,plain, % 116.74/116.81 (~P27(a7,x39331)+~E(x39331,a9)), % 116.74/116.81 inference(scs_inference,[],[876,71,686])). % 116.74/116.81 cnf(3950,plain, % 116.74/116.81 (~P19(a1,x39501)+P19(a7,x39502)+~E(x39501,x39502)), % 116.74/116.81 inference(scs_inference,[],[105,73,156])). % 116.74/116.81 cnf(3951,plain, % 116.74/116.81 (~P19(a1,x39511)+P19(a7,x39511)), % 116.74/116.81 inference(equality_inference,[],[3950])). % 116.74/116.81 cnf(3967,plain, % 116.74/116.81 (P19(a7,a5)), % 116.74/116.81 inference(scs_inference,[],[99,3951,118])). % 116.74/116.81 cnf(3968,plain, % 116.74/116.81 (~P36(a7,a5)), % 116.74/116.81 inference(scs_inference,[],[3967,146])). % 116.74/116.81 cnf(3970,plain, % 116.74/116.81 (~P12(a7,a5)), % 116.74/116.81 inference(scs_inference,[],[3967,146,137])). % 116.74/116.81 cnf(3974,plain, % 116.74/116.81 (~P6(a7,a5)), % 116.74/116.81 inference(scs_inference,[],[3967,146,137,138,135])). % 116.74/116.81 cnf(3982,plain, % 116.74/116.81 (~P31(a7,a5)), % 116.74/116.81 inference(scs_inference,[],[3967,146,137,138,135,136,134,116,133])). % 116.74/116.81 cnf(4035,plain, % 116.74/116.81 (~P36(a7,x40351)+~E(a5,x40351)), % 116.74/116.81 inference(scs_inference,[],[3967,73,146])). % 116.74/116.81 cnf(4102,plain, % 116.74/116.81 (~P27(a7,x41021)+~E(x41021,a7)), % 116.74/116.81 inference(scs_inference,[],[832,75,125])). % 116.74/116.81 cnf(4415,plain, % 116.74/116.81 (P12(a1,a6)), % 116.74/116.81 inference(scs_inference,[],[103,135])). % 116.74/116.81 cnf(4423,plain, % 116.74/116.81 (P12(a7,a6)), % 116.74/116.81 inference(scs_inference,[],[105,103,104,451,135,117,116,154,169])). % 116.74/116.81 cnf(4427,plain, % 116.74/116.81 (P3(a7,a4)), % 116.74/116.81 inference(scs_inference,[],[105,103,104,451,135,117,116,154,169,750,136])). % 116.74/116.81 cnf(4445,plain, % 116.74/116.81 (P3(a1,a3)), % 116.74/116.81 inference(scs_inference,[],[420,116,136])). % 116.74/116.81 cnf(4463,plain, % 116.74/116.81 (P3(a1,a4)), % 116.74/116.81 inference(scs_inference,[],[504,450,116,138,136])). % 116.74/116.81 cnf(4475,plain, % 116.74/116.81 (P6(a7,f10(a8))), % 116.74/116.81 inference(scs_inference,[],[2820,133])). % 116.74/116.81 cnf(4477,plain, % 116.74/116.81 (P36(a1,a7)), % 116.74/116.81 inference(scs_inference,[],[2820,503,133,138])). % 116.74/116.81 cnf(4479,plain, % 116.74/116.81 (P12(a7,f10(a8))), % 116.74/116.81 inference(scs_inference,[],[2820,503,133,138,135])). % 116.74/116.81 cnf(4496,plain, % 116.74/116.81 (P36(a7,a3)), % 116.74/116.81 inference(scs_inference,[],[480,138])). % 116.74/116.81 cnf(4515,plain, % 116.74/116.81 (P36(a7,a4)), % 116.74/116.81 inference(scs_inference,[],[4427,4477,146,138])). % 116.74/116.81 cnf(4520,plain, % 116.74/116.81 (P36(a7,a9)), % 116.74/116.81 inference(scs_inference,[],[792,3968,4427,4477,146,138,81,185,137])). % 116.74/116.81 cnf(4531,plain, % 116.74/116.81 (~P19(a7,a3)), % 116.74/116.81 inference(scs_inference,[],[789,4496,137,146])). % 116.74/116.81 cnf(4536,plain, % 116.74/116.81 (~P18(a7,a3)), % 116.74/116.81 inference(scs_inference,[],[789,4445,3968,4496,4520,137,146,138,81,118])). % 116.74/116.81 cnf(4545,plain, % 116.74/116.81 (P36(a1,a6)), % 116.74/116.81 inference(scs_inference,[],[4415,137])). % 116.74/116.81 cnf(4549,plain, % 116.74/116.81 (P36(a1,a4)), % 116.74/116.81 inference(scs_inference,[],[4415,4463,4515,137,146,138])). % 116.74/116.81 cnf(4551,plain, % 116.74/116.81 (P36(a7,a6)), % 116.74/116.81 inference(scs_inference,[],[105,4415,4463,4515,137,146,138,171])). % 116.74/116.81 cnf(4566,plain, % 116.74/116.81 (~P19(a7,a9)), % 116.74/116.81 inference(scs_inference,[],[4479,4520,137,146])). % 116.74/116.81 cnf(4583,plain, % 116.74/116.81 (~P18(a1,a3)), % 116.74/116.81 inference(scs_inference,[],[105,4536,4549,4531,146,156,155])). % 116.74/116.81 cnf(4597,plain, % 116.74/116.81 (~P19(a1,a9)), % 116.74/116.81 inference(scs_inference,[],[105,4551,4566,146,156])). % 116.74/116.81 cnf(4599,plain, % 116.74/116.81 (~P18(a7,a6)), % 116.74/116.81 inference(scs_inference,[],[105,4551,4566,146,156,118])). % 116.74/116.81 cnf(4611,plain, % 116.74/116.81 (~P29(a1,a9)), % 116.74/116.81 inference(scs_inference,[],[105,1216,4545,146,154])). % 116.74/116.81 cnf(4614,plain, % 116.74/116.81 (~P18(a1,a6)), % 116.74/116.81 inference(scs_inference,[],[105,99,4583,4599,1216,4545,146,154,29,155])). % 116.74/116.81 cnf(4620,plain, % 116.74/116.81 (~P30(a7,a7)), % 116.74/116.81 inference(scs_inference,[],[105,99,4583,4597,4599,3341,1216,4545,146,154,29,155,185,156,149])). % 116.74/116.81 cnf(4663,plain, % 116.74/116.82 (~P30(a1,a7)), % 116.74/116.82 inference(scs_inference,[],[105,102,99,792,504,789,3241,1224,4614,833,4620,130,29,131,2,128,132,185,157,160,165])). % 116.74/116.82 cnf(4679,plain, % 116.74/116.82 (P30(a1,a9)), % 116.74/116.82 inference(scs_inference,[],[789,128])). % 116.74/116.82 cnf(4744,plain, % 116.74/116.82 (P30(a7,f10(a8))), % 116.74/116.82 inference(scs_inference,[],[4479,128])). % 116.74/116.82 cnf(5763,plain, % 116.74/116.82 (P26(a7,a6)), % 116.74/116.82 inference(scs_inference,[],[4463,4423,139,141])). % 116.74/116.82 cnf(5765,plain, % 116.74/116.82 (P6(a7,f10(a5))), % 116.74/116.82 inference(scs_inference,[],[4463,4423,196,139,141,143])). % 116.74/116.82 cnf(5767,plain, % 116.74/116.82 (P31(a7,f10(a5))), % 116.74/116.82 inference(scs_inference,[],[4463,4423,196,139,141,143,144])). % 116.74/116.82 cnf(5769,plain, % 116.74/116.82 (P23(a7,f10(a8))), % 116.74/116.82 inference(scs_inference,[],[4463,4423,230,196,139,141,143,144,145])). % 116.74/116.82 cnf(5777,plain, % 116.74/116.82 (P13(a7,a8)), % 116.74/116.82 inference(scs_inference,[],[4679,4463,4423,4611,230,196,139,141,143,144,145,180,116,149,119])). % 116.74/116.82 cnf(5779,plain, % 116.74/116.82 (~P15(a7,a6)), % 116.74/116.82 inference(scs_inference,[],[4679,4463,4423,4611,230,196,139,141,143,144,145,180,116,149,119,718])). % 116.74/116.82 cnf(5787,plain, % 116.74/116.82 (P27(a7,a8)), % 116.74/116.82 inference(scs_inference,[],[4679,4463,4423,4611,4663,230,196,139,141,143,144,145,180,116,149,119,718,140,115,128,122])). % 116.74/116.82 cnf(5789,plain, % 116.74/116.82 (~P6(a1,a7)), % 116.74/116.82 inference(scs_inference,[],[4679,4463,4423,4611,4663,230,196,139,141,143,144,145,180,116,149,119,718,140,115,128,122,135])). % 116.74/116.82 cnf(5791,plain, % 116.74/116.82 (P19(a7,a8)), % 116.74/116.82 inference(scs_inference,[],[4679,4463,4423,4611,4663,230,196,139,141,143,144,145,180,116,149,119,718,140,115,128,122,135,118])). % 116.74/116.82 cnf(5795,plain, % 116.74/116.82 (P15(a7,a4)), % 116.74/116.82 inference(scs_inference,[],[4679,4463,4423,4611,876,4663,230,196,105,139,141,143,144,145,180,116,149,119,718,140,115,128,122,135,118,164,172])). % 116.74/116.82 cnf(5807,plain, % 116.74/116.82 (~P36(a1,a5)), % 116.74/116.82 inference(scs_inference,[],[1229,3344,1227,3970,4679,4463,4423,4611,3968,876,4663,230,196,105,139,141,143,144,145,180,116,149,119,718,140,115,128,122,135,118,164,172,173,167,152,169,150,171])). % 116.74/116.82 cnf(5811,plain, % 116.74/116.82 (~P6(a1,a5)), % 116.74/116.82 inference(scs_inference,[],[1229,3344,1227,3974,3982,3970,4679,4463,4423,4611,3968,876,4663,230,196,105,139,141,143,144,145,180,116,149,119,718,140,115,128,122,135,118,164,172,173,167,152,169,150,171,177,168])). % 116.74/116.82 cnf(5813,plain, % 116.74/116.82 (~P7(a7,f10(a8),f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.74/116.82 inference(scs_inference,[],[94,1229,3344,1227,3974,3982,3970,4679,4475,4463,4423,4611,1883,3968,876,4663,230,196,95,103,98,107,112,101,2820,99,102,110,104,97,105,111,106,96,109,108,139,141,143,144,145,180,116,149,119,718,140,115,128,122,135,118,164,172,173,167,152,169,150,171,177,168,189])). % 116.74/116.82 cnf(5819,plain, % 116.74/116.82 (~P13(a7,a4)), % 116.74/116.82 inference(scs_inference,[],[94,1229,3344,1227,3974,3982,3970,4679,4475,4463,4423,4611,1883,3968,876,4663,230,196,95,103,98,107,112,101,2820,99,102,110,104,97,105,111,106,96,109,108,139,141,143,144,145,180,116,149,119,718,140,115,128,122,135,118,164,172,173,167,152,169,150,171,177,168,189,124,638,1129])). % 116.74/116.82 cnf(5826,plain, % 116.74/116.82 (P11(a7,a8)), % 116.74/116.82 inference(scs_inference,[],[5777,5787,121,686])). % 116.74/116.82 cnf(5834,plain, % 116.74/116.82 (P13(a7,a5)), % 116.74/116.82 inference(scs_inference,[],[5777,5787,5811,4445,4415,196,121,686,132,139,141,119])). % 116.74/116.82 cnf(5836,plain, % 116.74/116.82 (~P15(a7,f10(a8))), % 116.74/116.82 inference(scs_inference,[],[5777,5787,5811,4744,4445,4415,196,121,686,132,139,141,119,149])). % 116.74/116.82 cnf(5842,plain, % 116.74/116.82 (P10(a7,a8)), % 116.74/116.82 inference(scs_inference,[],[5777,5787,5811,4744,4445,4415,196,792,121,686,132,139,141,119,149,718,140,125])). % 116.74/116.82 cnf(5848,plain, % 116.74/116.82 (P27(a7,a5)), % 116.74/116.82 inference(scs_inference,[],[5777,5787,5789,5791,5811,4744,4445,4415,196,792,121,686,132,139,141,119,149,718,140,125,146,133,122])). % 116.74/116.82 cnf(5852,plain, % 116.74/116.82 (~P6(a7,a8)), % 116.74/116.82 inference(scs_inference,[],[5777,5787,5789,5791,5811,4744,4445,4415,196,792,121,686,132,139,141,119,149,718,140,125,146,133,122,137,135])). % 116.74/116.82 cnf(5876,plain, % 116.74/116.82 (~P15(a7,a8)), % 116.74/116.82 inference(scs_inference,[],[5777,5787,5789,5791,5811,5819,5813,1215,4744,4445,4415,196,792,101,105,121,686,132,139,141,119,149,718,140,125,146,133,122,137,135,118,183,157,170,129,148,124,3325,1129,638,127,702])). % 116.74/116.82 cnf(5882,plain, % 116.74/116.82 (~E(a4,a6)), % 116.74/116.82 inference(scs_inference,[],[94,5779,5777,5787,5789,5791,5795,5811,5819,5813,5767,3348,1215,4744,4445,4415,196,792,101,105,121,686,132,139,141,119,149,718,140,125,146,133,122,137,135,118,183,157,170,129,148,124,3325,1129,638,127,702,138,18,40,63])). % 116.74/116.82 cnf(5890,plain, % 116.74/116.82 (~P5(a7,a8)), % 116.74/116.82 inference(scs_inference,[],[94,5779,5777,5787,5789,5791,5795,5811,5819,5765,5813,5767,3348,1215,3974,4744,4445,4415,196,792,101,105,121,686,132,139,141,119,149,718,140,125,146,133,122,137,135,118,183,157,170,129,148,124,3325,1129,638,127,702,138,18,40,63,38,3168,136,116,115])). % 116.74/116.82 cnf(5907,plain, % 116.74/116.82 (P15(a7,a3)), % 116.74/116.82 inference(scs_inference,[],[5834,5848,5852,5876,480,121,686,132,3325,148,139])). % 116.74/116.82 cnf(5911,plain, % 116.74/116.82 (P13(a1,a8)), % 116.74/116.82 inference(scs_inference,[],[5834,5848,5852,5876,4479,480,101,121,686,132,3325,148,139,141,119])). % 116.74/116.82 cnf(5919,plain, % 116.74/116.82 (P27(a1,a8)), % 116.74/116.82 inference(scs_inference,[],[5834,5848,5852,5876,4479,480,101,121,686,132,3325,148,139,141,119,140,125,133,122])). % 116.74/116.82 cnf(5933,plain, % 116.74/116.82 (~P15(a7,a5)), % 116.74/116.82 inference(scs_inference,[],[5834,5848,5852,5876,4479,480,101,99,121,686,132,3325,148,139,141,119,140,125,133,122,118,3168,129,124,638,127,149])). % 116.74/116.82 cnf(5949,plain, % 116.74/116.82 (P15(a1,a7)), % 116.74/116.82 inference(scs_inference,[],[5933,5911,5919,503,789,121,686,3325,141,139])). % 116.74/116.82 cnf(6240,plain, % 116.74/116.82 (P18(a7,f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.74/116.82 inference(scs_inference,[],[94,5807,5769,4475,1883,103,95,98,107,112,2820,101,102,99,97,110,104,105,111,106,96,108,109,80,188])). % 116.74/116.82 cnf(6242,plain, % 116.74/116.82 (P13(a7,f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.74/116.82 inference(scs_inference,[],[94,5807,5769,4475,1883,103,95,98,107,112,2820,101,102,99,97,110,104,105,111,106,96,108,109,80,188,119])). % 116.74/116.82 cnf(6246,plain, % 116.74/116.82 (P19(a7,f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.74/116.82 inference(scs_inference,[],[94,5807,5769,4475,1883,103,95,98,107,112,2820,101,102,99,97,110,104,105,111,106,96,108,109,80,188,119,638,118])). % 116.74/116.82 cnf(6248,plain, % 116.74/116.82 (P27(a7,f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.74/116.82 inference(scs_inference,[],[94,5807,5769,4475,1883,103,95,98,107,112,2820,101,102,99,97,110,104,105,111,106,96,108,109,80,188,119,638,118,122])). % 116.74/116.82 cnf(6250,plain, % 116.74/116.82 (P10(a7,f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.74/116.82 inference(scs_inference,[],[94,5807,5769,4475,1883,103,95,98,107,112,2820,101,102,99,97,110,104,105,111,106,96,108,109,80,188,119,638,118,122,125])). % 116.74/116.82 cnf(6282,plain, % 116.74/116.82 (~P36(a1,f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.74/116.82 inference(scs_inference,[],[6242,6246,6248,6250,105,3933,4102,121,702,686,3325,124,148,127,129,146,137,135,171])). % 116.74/116.82 cnf(6284,plain, % 116.74/116.82 (~P6(a1,f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.74/116.82 inference(scs_inference,[],[6242,6246,6248,6250,105,3933,4102,121,702,686,3325,124,148,127,129,146,137,135,171,168])). % 116.74/116.82 cnf(6298,plain, % 116.74/116.82 (~P3(a7,f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.74/116.82 inference(scs_inference,[],[6242,6246,6248,6250,5765,5949,105,3933,4102,121,702,686,3325,124,148,127,129,146,137,135,171,168,169,38,63,3188,342,1479,132,3168,138])). % 116.74/116.82 cnf(6300,plain, % 116.74/116.82 (~P31(a7,f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.74/116.82 inference(scs_inference,[],[6242,6246,6248,6250,5765,5949,105,3933,4102,121,702,686,3325,124,148,127,129,146,137,135,171,168,169,38,63,3188,342,1479,132,3168,138,133])). % 116.74/116.82 cnf(6346,plain, % 116.74/116.82 (~P5(a7,f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.74/116.82 inference(scs_inference,[],[6282,6284,6298,136,132,116,138,115])). % 116.74/116.82 cnf(6354,plain, % 116.74/116.82 (~P5(a1,f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.74/116.82 inference(scs_inference,[],[6282,6284,6298,105,136,132,116,138,115,117,133,153,151])). % 116.74/116.82 cnf(6983,plain, % 116.74/116.82 (~P7(a7,f10(a5),f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.74/116.82 inference(scs_inference,[],[104,1883,4475,94,5769,112,5765,95,2820,103,5767,1750,98,101,102,99,107,110,97,105,111,106,96,108,109,189])). % 116.74/116.82 cnf(6996,plain, % 116.74/116.82 (~P7(a7,x69961,f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7))+~E(x69961,f10(a5))), % 116.74/116.82 inference(scs_inference,[],[6983,48])). % 116.74/116.82 cnf(7922,plain, % 116.74/116.82 (~P11(a7,a6)), % 116.74/116.82 inference(scs_inference,[],[5763,148])). % 116.74/116.82 cnf(7931,plain, % 116.74/116.82 (~P10(a1,a6)), % 116.74/116.82 inference(scs_inference,[],[7922,105,126,686,164,163])). % 116.74/116.82 cnf(7937,plain, % 116.74/116.82 (P12(a7,f10(a5))), % 116.74/116.82 inference(scs_inference,[],[5765,135])). % 116.74/116.82 cnf(7943,plain, % 116.74/116.82 (~P15(a1,f10(a5))), % 116.74/116.82 inference(scs_inference,[],[5765,135,750,718,3325])). % 116.74/116.82 cnf(7945,plain, % 116.74/116.82 (P26(a7,f10(a5))), % 116.74/116.82 inference(scs_inference,[],[5765,135,750,718,3325,141])). % 116.74/116.82 cnf(7955,plain, % 116.74/116.82 (~P27(a1,a6)), % 116.74/116.82 inference(scs_inference,[],[7931,125])). % 116.74/116.82 cnf(7962,plain, % 116.74/116.82 (~P10(a7,f10(a5))), % 116.74/116.82 inference(scs_inference,[],[7943,7945,148,139,126])). % 116.74/116.82 cnf(7964,plain, % 116.74/116.82 (~P29(a1,f10(a5))), % 116.74/116.82 inference(scs_inference,[],[7943,7945,148,139,126,136])). % 116.74/116.82 cnf(7966,plain, % 116.74/116.82 (~P28(a1,f10(a5))), % 116.74/116.82 inference(scs_inference,[],[7943,7945,148,139,126,136,116])). % 116.74/116.82 cnf(7981,plain, % 116.74/116.82 (~P10(a1,f10(a5))), % 116.74/116.82 inference(scs_inference,[],[7966,7962,7964,5842,105,424,117,75,163])). % 116.74/116.82 cnf(7992,plain, % 116.74/116.82 (~P30(a7,a3)), % 116.74/116.82 inference(scs_inference,[],[5907,149])). % 116.74/116.82 cnf(8000,plain, % 116.74/116.82 (~P27(a1,f10(a5))), % 116.74/116.82 inference(scs_inference,[],[7981,125])). % 116.74/116.82 cnf(8149,plain, % 116.74/116.82 (~P3(a7,f10(a8))), % 116.74/116.82 inference(scs_inference,[],[7955,7937,5836,137,122,139])). % 116.74/116.82 cnf(8163,plain, % 116.74/116.82 (~P5(a7,f10(a8))), % 116.74/116.82 inference(scs_inference,[],[8149,136,116,115])). % 116.74/116.82 cnf(8189,plain, % 116.74/116.82 (~P3(a7,a6)), % 116.74/116.82 inference(scs_inference,[],[8000,5779,122,139])). % 116.74/116.82 cnf(8191,plain, % 116.74/116.82 (~P4(a7,f10(a8))), % 116.74/116.82 inference(scs_inference,[],[8163,8000,5779,122,139,113])). % 116.74/116.82 cnf(8205,plain, % 116.74/116.82 (~P5(a7,a6)), % 116.74/116.82 inference(scs_inference,[],[8189,8191,105,150,136,116,115])). % 116.74/116.82 cnf(8298,plain, % 116.74/116.82 (~P4(a7,a6)), % 116.74/116.82 inference(scs_inference,[],[8205,113])). % 116.74/116.82 cnf(8308,plain, % 116.74/116.82 (~P4(a1,a6)), % 116.74/116.82 inference(scs_inference,[],[8298,105,150])). % 116.74/116.82 cnf(8331,plain, % 116.74/116.82 (P23(a7,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[6240,145])). % 116.74/116.82 cnf(8333,plain, % 116.74/116.82 (P31(a7,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[6240,145,144])). % 116.74/116.82 cnf(8335,plain, % 116.74/116.82 (P6(a7,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[6240,145,144,133])). % 116.74/116.82 cnf(8337,plain, % 116.74/116.82 (P7(a7,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)),f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.74/116.82 inference(scs_inference,[],[6240,145,144,133,180])). % 116.74/116.82 cnf(8341,plain, % 116.74/116.82 (P12(a7,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[6354,6240,145,144,133,180,113,135])). % 116.74/116.82 cnf(8346,plain, % 116.74/116.82 (P26(a7,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[8308,6354,6240,145,144,133,180,113,135,19,6996,2,141])). % 116.74/116.82 cnf(8348,plain, % 116.74/116.82 (P30(a7,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[8308,6354,6240,145,144,133,180,113,135,19,6996,2,141,128])). % 116.74/116.82 cnf(8358,plain, % 116.74/116.82 (P36(a7,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[8341,750,137])). % 116.74/116.82 cnf(8368,plain, % 116.74/116.82 (~P3(a7,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[8341,8346,750,137,718,130,3325,148,139])). % 116.74/116.82 cnf(8372,plain, % 116.74/116.82 (~P3(a1,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[8341,8346,8348,7992,5826,105,750,137,718,130,3325,148,139,91,71,170])). % 116.74/116.82 cnf(8378,plain, % 116.74/116.82 (~P10(a7,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[8333,8341,8346,8348,7992,5826,6300,105,750,137,718,130,3325,148,139,91,71,170,40,4035,506,126])). % 116.74/116.82 cnf(8380,plain, % 116.74/116.82 (~P27(a7,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[8333,8341,8346,8348,7992,5826,6300,105,750,137,718,130,3325,148,139,91,71,170,40,4035,506,126,686])). % 116.74/116.82 cnf(8393,plain, % 116.74/116.82 (~P10(a1,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[8378,105,163])). % 116.74/116.82 cnf(8399,plain, % 116.74/116.82 (~P29(a7,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[8380,8358,8368,8378,105,163,146,122,136])). % 116.74/116.82 cnf(8405,plain, % 116.74/116.82 (~P27(a1,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[8380,8358,8368,8378,5890,105,163,146,122,136,114,119,125])). % 116.74/116.82 cnf(8410,plain, % 116.74/116.82 (~P19(a1,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[8380,8358,8368,8378,8346,5890,6240,105,163,146,122,136,114,119,125,175,29,3951])). % 116.74/116.82 cnf(8412,plain, % 116.74/116.82 (~P28(a7,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[8380,8358,8368,8378,8346,5890,6240,105,163,146,122,136,114,119,125,175,29,3951,116])). % 116.74/116.82 cnf(8422,plain, % 116.74/116.82 (~P5(a7,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.74/116.82 inference(scs_inference,[],[8399,8412,105,117,153,115])). % 116.74/116.82 cnf(8425,plain, % 116.74/116.82 (~P7(a7,f10(f2(a1,a8,a3,a4,a5,a4,a6,a7,a3,a8,a9,a6,a7)),a8)), % 116.74/116.82 inference(scs_inference,[],[8331,8399,8393,8412,8337,8333,8335,111,106,112,94,102,103,95,110,98,101,99,108,109,107,97,96,104,105,117,153,115,74,189])). % 116.74/116.82 cnf(8448,plain, % 116.74/116.82 ($false), % 116.74/116.82 inference(scs_inference,[],[94,105,104,97,96,107,101,108,109,99,98,110,95,103,5769,102,4475,2820,112,1883,106,111,5882,4620,8333,8331,8335,6346,8348,8337,8425,8372,8410,8422,8405,114,136,122,118,113,117,185,1885,91,189]), % 116.74/116.82 ['proof']). % 116.74/116.82 % SZS output end Proof % 116.74/116.82 % Total time :116.120000s %------------------------------------------------------------------------------