%------------------------------------------------------------------------------ % File : iProver---3.9.4 % Problem : NLP013-1 : TPTP v9.3.1. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Sep 25 02:16:13 PM UTC 2026 % Result : Satisfiable 0.68s 1.14s % Output : Model 0.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NLP013-1 : TPTP v9.3.1. Released v2.4.0. % 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM % 0.11/0.37 % Computer : n007.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Thu Sep 24 01:36:37 UTC 2026 % 0.11/0.37 % CPUTime : % 0.11/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM % 0.11/0.41 Running EPR theorem proving % 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s epr_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.11/0.42 % 0.11/0.42 % ======== iProver multi-core TPTP/SMT ========= % 0.11/0.42 % 0.11/0.42 % Detected problem language: tptp % 0.11/0.44 % Proving... % 0.68/1.14 % SZS status Started for theBenchmark.p % 0.68/1.14 % SZS status Satisfiable for theBenchmark.p % 0.68/1.14 % 0.68/1.14 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------% % 0.68/1.14 % 0.68/1.14 % ------ iProver source info % 0.68/1.14 % 0.68/1.14 % git: date: 2026-07-19 20:42:38 +0200 % 0.68/1.14 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61 % 0.68/1.14 % git: non_committed_changes: false % 0.68/1.14 % 0.68/1.14 % ------ Parsing...% successful % 0.68/1.14 % 0.68/1.14 % 0.68/1.14 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_eq % 0.68/1.14 % % 0.68/1.14 % 0.68/1.14 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 0 sf_s rm: 14 0s sf_e pe_s pe_e % % 0.68/1.14 % 0.68/1.14 % ------ Preprocessing...% ------ preprocesses with Option_epr_non_horn_eq % 0.68/1.14 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e % ------ preprocesses with Option_epr_non_horn_eq % 0.68/1.14 % % 0.68/1.14 % 0.68/1.14 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e % 0.68/1.14 % ------ Proving... % 0.68/1.14 % ------ Problem Properties % 0.68/1.14 % 0.68/1.14 % % 0.68/1.14 % clauses 31 % 0.68/1.14 % conjectures 29 % 0.68/1.14 % EPR 31 % 0.68/1.14 % Horn 21 % 0.68/1.14 % unary 7 % 0.68/1.14 % binary 22 % 0.68/1.14 % lits 80 % 0.68/1.14 % lits eq 4 % 0.68/1.14 % fd_pure 0 % 0.68/1.14 % fd_pseudo 0 % 0.68/1.14 % fd_cond 0 % 0.68/1.14 % fd_pseudo_cond 2 % 0.68/1.14 % AC symbols 0 % 0.68/1.14 % 0.68/1.14 % ------ Schedule EPR non Horn eq is on % 0.68/1.14 % 0.68/1.14 % ------ Option_epr_non_horn_eq Time Limit: Unbounded % 0.68/1.14 % 0.68/1.14 % 0.68/1.14 % ------ % 0.68/1.14 % Current options: % 0.68/1.14 % ------ % 0.68/1.14 % 0.68/1.14 % 0.68/1.14 % % 0.68/1.14 % 0.68/1.14 % ------ Proving... % 0.68/1.14 % % 0.68/1.14 % 0.68/1.14 % SZS status Satisfiable for theBenchmark.p % 0.68/1.14 % 0.68/1.14 ------ Building Model...Done % 0.68/1.14 % 0.68/1.14 %------ The model is defined over ground terms (initial term algebra). % 0.68/1.14 %------ Predicates are defined as (\forall x_1,..,x_n ((~)P(x_1,..,x_n) <=> (\phi(x_1,..,x_n)))) % 0.68/1.14 %------ where \phi is a formula over the term algebra. % 0.68/1.14 %------ If we have equality in the problem then it is also defined as a predicate above, % 0.68/1.14 %------ with "=" on the right-hand-side of the definition interpreted over the term algebra term_algebra_type % 0.68/1.14 %------ See help for --sat_out_model for different model outputs. % 0.68/1.14 %------ equality_sorted(X0,X1,X2) can be used in the place of usual "=" % 0.68/1.14 %------ where the first argument stands for the sort ($i in the unsorted case) % 0.68/1.14 % SZS output start Model for theBenchmark.p % 0.68/1.14 % 0.68/1.14 %------ Positive definition of equality_sorted % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0_tType,X0_o,X1_o] : % 0.68/1.14 ( equality_sorted(X0_tType,X0_o,X1_o) <=> % 0.68/1.14 ( % 0.68/1.14 ( % 0.68/1.14 ( X0_tType=$o & X1_o=X0_o ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 | % 0.68/1.14 ( % 0.68/1.14 ( X0_tType=iProver_young_1 ) % 0.68/1.14 & % 0.68/1.14 ( X0_iProver_young_1!=skc21 ) % 0.68/1.14 & % 0.68/1.14 ( X0_iProver_young_1!=skc21 | X1_iProver_young_1!=skc15 ) % 0.68/1.14 & % 0.68/1.14 ( X0_iProver_young_1!=skc16 ) % 0.68/1.14 & % 0.68/1.14 ( X0_iProver_young_1!=skc16 | X1_iProver_young_1!=skc15 ) % 0.68/1.14 & % 0.68/1.14 ( X1_iProver_young_1!=skc21 ) % 0.68/1.14 & % 0.68/1.14 ( X1_iProver_young_1!=skc16 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 | % 0.68/1.14 ( % 0.68/1.14 ( X0_tType=iProver_young_1 & X0_iProver_young_1=skc21 & X1_iProver_young_1=skc21 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 | % 0.68/1.14 ( % 0.68/1.14 ( X0_tType=iProver_young_1 & X0_iProver_young_1=skc16 & X1_iProver_young_1=skc16 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 | % 0.68/1.14 ( % 0.68/1.14 ( X0_tType=iProver_young_1 & X1_iProver_young_1=skc15 ) % 0.68/1.14 & % 0.68/1.14 ( X0_iProver_young_1!=skc21 ) % 0.68/1.14 & % 0.68/1.14 ( X0_iProver_young_1!=skc16 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 | % 0.68/1.14 ( % 0.68/1.14 ( X0_tType=iProver_young_1 & X1_iProver_young_1=X0_iProver_young_1 ) % 0.68/1.14 & % 0.68/1.14 ( X0_iProver_young_1!=skc21 ) % 0.68/1.14 & % 0.68/1.14 ( X0_iProver_young_1!=skc16 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of hollywood % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0] : % 0.68/1.14 ( hollywood(X0) <=> % 0.68/1.14 $false % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of event % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0] : % 0.68/1.14 ( event(X0) <=> % 0.68/1.14 $false % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of chevy % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0] : % 0.68/1.14 ( chevy(X0) <=> % 0.68/1.14 $false % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of lonely % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0] : % 0.68/1.14 ( lonely(X0) <=> % 0.68/1.14 $false % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of seat % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0_iProver_seat_1] : % 0.68/1.14 ( seat(X0_iProver_seat_1) <=> % 0.68/1.14 ( % 0.68/1.14 ( % 0.68/1.14 ( X0_iProver_seat_1=skc25 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 | % 0.68/1.14 ( % 0.68/1.14 ( X0_iProver_seat_1=skc18 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 | % 0.68/1.14 ( % 0.68/1.14 ( X0_iProver_seat_1=skc17 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of young % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0_iProver_young_1] : % 0.68/1.14 ( young(X0_iProver_young_1) <=> % 0.68/1.14 $true % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of fellow % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0_iProver_young_1] : % 0.68/1.14 ( fellow(X0_iProver_young_1) <=> % 0.68/1.14 $true % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of city % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0] : % 0.68/1.14 ( city(X0) <=> % 0.68/1.14 $false % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of front % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0_iProver_seat_1] : % 0.68/1.14 ( front(X0_iProver_seat_1) <=> % 0.68/1.14 ( % 0.68/1.14 ( % 0.68/1.14 ( X0_iProver_seat_1=skc18 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 | % 0.68/1.14 ( % 0.68/1.14 ( X0_iProver_seat_1=skc17 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of ssSkC0 % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 ( ssSkC0 <=> % 0.68/1.14 $true % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of street % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0] : % 0.68/1.14 ( street(X0) <=> % 0.68/1.14 $false % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of way % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0] : % 0.68/1.14 ( way(X0) <=> % 0.68/1.14 $false % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of old % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0] : % 0.68/1.14 ( old(X0) <=> % 0.68/1.14 $false % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of dirty % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0] : % 0.68/1.14 ( dirty(X0) <=> % 0.68/1.14 $false % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of white % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0] : % 0.68/1.14 ( white(X0) <=> % 0.68/1.14 $false % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of car % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0] : % 0.68/1.14 ( car(X0) <=> % 0.68/1.14 $false % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of man % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0_iProver_young_1] : % 0.68/1.14 ( man(X0_iProver_young_1) <=> % 0.68/1.14 ( % 0.68/1.14 ( % 0.68/1.14 ( X0_iProver_young_1!=skc21 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 | % 0.68/1.14 ( % 0.68/1.14 ( X0_iProver_young_1=skc16 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 | % 0.68/1.14 ( % 0.68/1.14 ( X0_iProver_young_1=skc15 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of furniture % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0_iProver_seat_1] : % 0.68/1.14 ( furniture(X0_iProver_seat_1) <=> % 0.68/1.14 ( % 0.68/1.14 ( % 0.68/1.14 ( X0_iProver_seat_1=skc18 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 | % 0.68/1.14 ( % 0.68/1.14 ( X0_iProver_seat_1=skc17 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of barrel % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0,X1] : % 0.68/1.14 ( barrel(X0,X1) <=> % 0.68/1.14 $false % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of down % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0,X1] : % 0.68/1.14 ( down(X0,X1) <=> % 0.68/1.14 $false % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % 0.68/1.14 %------ Positive definition of in % 0.68/1.14 fof(lit_def,axiom, % 0.68/1.14 (! [X0_iProver_young_1,X0_iProver_seat_1] : % 0.68/1.14 ( in(X0_iProver_young_1,X0_iProver_seat_1) <=> % 0.68/1.14 ( % 0.68/1.14 ( % 0.68/1.14 ( X0_iProver_young_1=skc21 & X0_iProver_seat_1=skc22 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 | % 0.68/1.14 ( % 0.68/1.14 ( X0_iProver_young_1=skc16 & X0_iProver_seat_1=skc17 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 | % 0.68/1.14 ( % 0.68/1.14 ( X0_iProver_young_1=skc15 & X0_iProver_seat_1=skc18 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 | % 0.68/1.14 ( % 0.68/1.14 ( X0_iProver_seat_1=skc18 ) % 0.68/1.14 & % 0.68/1.14 ( X0_iProver_young_1!=skc16 ) % 0.68/1.14 ) % 0.68/1.14 % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ) % 0.68/1.14 ). % 0.68/1.14 % SZS output end Model for theBenchmark.p % 0.68/1.14 %------------------------------------------------------------------------------