%------------------------------------------------------------------------------
% File : FEST---2.0.1
% Problem : SWW679_1 : TPTP v9.0.0. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fest %s %d
% Computer : n003.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 : Sat Mar 29 08:52:01 AM UTC 2025
% Result : Timeout 5.81s 300.06s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWW679_1 : TPTP v9.0.0. Released v6.4.0.
% 0.07/0.12 % Command : run_fest %s %d
% 0.12/0.34 % Computer : n003.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Mar 28 21:40:34 EDT 2025
% 0.12/0.34 % CPUTime :
% 5.81/300.06 Alarm clock
% 5.81/300.07 RuntimeError("Could not parse (declare-sort tptp.'Tree' 0)\n(declare-fun tptp.searchtree (|tptp.'Tree'|) Bool)\n(declare-fun |tptp.'right:(Tree)>Tree'| (|tptp.'Tree'|) |tptp.'Tree'|)\n(declare-fun |tptp.'val:(Tree)>Int'| (|tptp.'Tree'|) Int)\n(declare-fun |tptp.'left:(Tree)>Tree'| (|tptp.'Tree'|) |tptp.'Tree'|)\n(declare-fun |tptp.'empty:Tree'| () |tptp.'Tree'|)\n(declare-fun tptp.in (Int |tptp.'Tree'|) Bool)\n(declare-fun |tptp.'node:(Int*Tree*Tree)>Tree'|\n (Int |tptp.'Tree'| |tptp.'Tree'|)\n |tptp.'Tree'|)\n(assert (let ((a!1 (forall ((X |tptp.'Tree'|))\n (or (= X |tptp.'empty:Tree'|)\n (= X\n (|tptp.'node:(Int*Tree*Tree)>Tree'|\n (|tptp.'val:(Tree)>Int'| X)\n (|tptp.'left:(Tree)>Tree'| X)\n (|tptp.'right:(Tree)>Tree'| X))))))\n (a!2 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'val:(Tree)>Int'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_0)))\n (a!3 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'left:(Tree)>Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_1)))\n (a!4 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'right:(Tree)>Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_2)))\n (a!5 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (not (= |tptp.'empty:Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2)))))\n (a!6 (forall ((V Int) (T |tptp.'Tree'|))\n (let ((a!1 (=> (not (= T |tptp.'empty:Tree'|))\n (or (= V (|tptp.'val:(Tree)>Int'| T))\n (tptp.in V (|tptp.'left:(Tree)>Tree'| T))\n (tptp.in V (|tptp.'right:(Tree)>Tree'| T))))))\n (= (tptp.in V T) (and (=> (= T |tptp.'empty:Tree'|) false) a!1)))))\n (a!7 (forall ((T |tptp.'Tree'|))\n (let ((a!1 (forall ((V Int))\n (=> (tptp.in V (|tptp.'left:(Tree)>Tree'| T))\n (<= V (|tptp.'val:(Tree)>Int'| T)))))\n (a!2 (forall ((V Int))\n (=> (tptp.in V (|tptp.'right:(Tree)>Tree'| T))\n (> V (|tptp.'val:(Tree)>Int'| T))))))\n (let ((a!3 (=> (not (= T |tptp.'empty:Tree'|))\n (and (tptp.searchtree (|tptp.'left:(Tree)>Tree'| T))\n (tptp.searchtree (|tptp.'right:(Tree)>Tree'| T))\n a!1\n a!2))))\n (= (tptp.searchtree T)\n (and (=> (= T |tptp.'empty:Tree'|) true) a!3))))))\n (a!8 (not (forall ((T |tptp.'Tree'|) (V Int))\n (let ((a!1 (exists ((T_1 |tptp.'Tree'|))\n (and (= T_1 (|tptp.'left:(Tree)>Tree'| T))\n (tptp.searchtree T_1))))\n (a!2 (exists ((T_2 |tptp.'Tree'|))\n (and (= T_2 (|tptp.'right:(Tree)>Tree'| T))\n (tptp.searchtree T_2)))))\n (let ((a!3 (=> (not (< V (|tptp.'val:(Tree)>Int'| T))) a!2)))\n (let ((a!4 (and (=> (< V (|tptp.'val:(Tree)>Int'| T)) a!1)\n a!3)))\n (let ((a!5 (=> (not (= V (|tptp.'val:(Tree)>Int'| T))) a!4)))\n (let ((a!6 (and (=> (= V (|tptp.'val:(Tree)>Int'| T)) true)\n a!5)))\n (let ((a!7 (and (=> (= T |tptp.'empty:Tree'|) true)\n (=> (not (= T |tptp.'empty:Tree'|)) a!6))))\n (=> (tptp.searchtree T) a!7)))))))))))\n (= (and a!1 a!2 a!3 a!4 a!5 a!6 a!7 a!8)\n (and a!1 a!2 a!3 a!4 a!5 a!6 a!7 a!8))))\n")
% 5.81/300.07 RuntimeError("Could not parse (declare-sort tptp.'Tree' 0)\n(declare-fun tptp.searchtree (|tptp.'Tree'|) Bool)\n(declare-fun |tptp.'right:(Tree)>Tree'| (|tptp.'Tree'|) |tptp.'Tree'|)\n(declare-fun |tptp.'val:(Tree)>Int'| (|tptp.'Tree'|) Int)\n(declare-fun |tptp.'left:(Tree)>Tree'| (|tptp.'Tree'|) |tptp.'Tree'|)\n(declare-fun |tptp.'empty:Tree'| () |tptp.'Tree'|)\n(declare-fun tptp.in (Int |tptp.'Tree'|) Bool)\n(declare-fun |tptp.'node:(Int*Tree*Tree)>Tree'|\n (Int |tptp.'Tree'| |tptp.'Tree'|)\n |tptp.'Tree'|)\n(assert (let ((a!1 (forall ((X |tptp.'Tree'|))\n (or (= X |tptp.'empty:Tree'|)\n (= X\n (|tptp.'node:(Int*Tree*Tree)>Tree'|\n (|tptp.'val:(Tree)>Int'| X)\n (|tptp.'left:(Tree)>Tree'| X)\n (|tptp.'right:(Tree)>Tree'| X))))))\n (a!2 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'val:(Tree)>Int'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_0)))\n (a!3 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'left:(Tree)>Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_1)))\n (a!4 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'right:(Tree)>Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_2)))\n (a!5 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (not (= |tptp.'empty:Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2)))))\n (a!6 (forall ((V Int) (T |tptp.'Tree'|))\n (let ((a!1 (=> (not (= T |tptp.'empty:Tree'|))\n (or (= V (|tptp.'val:(Tree)>Int'| T))\n (tptp.in V (|tptp.'left:(Tree)>Tree'| T))\n (tptp.in V (|tptp.'right:(Tree)>Tree'| T))))))\n (= (tptp.in V T) (and (=> (= T |tptp.'empty:Tree'|) false) a!1)))))\n (a!7 (forall ((T |tptp.'Tree'|))\n (let ((a!1 (forall ((V Int))\n (=> (tptp.in V (|tptp.'left:(Tree)>Tree'| T))\n (<= V (|tptp.'val:(Tree)>Int'| T)))))\n (a!2 (forall ((V Int))\n (=> (tptp.in V (|tptp.'right:(Tree)>Tree'| T))\n (> V (|tptp.'val:(Tree)>Int'| T))))))\n (let ((a!3 (=> (not (= T |tptp.'empty:Tree'|))\n (and (tptp.searchtree (|tptp.'left:(Tree)>Tree'| T))\n (tptp.searchtree (|tptp.'right:(Tree)>Tree'| T))\n a!1\n a!2))))\n (= (tptp.searchtree T)\n (and (=> (= T |tptp.'empty:Tree'|) true) a!3))))))\n (a!8 (not (forall ((T |tptp.'Tree'|) (V Int))\n (let ((a!1 (exists ((T_1 |tptp.'Tree'|))\n (and (= T_1 (|tptp.'left:(Tree)>Tree'| T))\n (tptp.searchtree T_1))))\n (a!2 (exists ((T_2 |tptp.'Tree'|))\n (and (= T_2 (|tptp.'right:(Tree)>Tree'| T))\n (tptp.searchtree T_2)))))\n (let ((a!3 (=> (not (< V (|tptp.'val:(Tree)>Int'| T))) a!2)))\n (let ((a!4 (and (=> (< V (|tptp.'val:(Tree)>Int'| T)) a!1)\n a!3)))\n (let ((a!5 (=> (not (= V (|tptp.'val:(Tree)>Int'| T))) a!4)))\n (let ((a!6 (and (=> (= V (|tptp.'val:(Tree)>Int'| T)) true)\n a!5)))\n (let ((a!7 (and (=> (= T |tptp.'empty:Tree'|) true)\n (=> (not (= T |tptp.'empty:Tree'|)) a!6))))\n (=> (tptp.searchtree T) a!7)))))))))))\n (= (and a!1 a!2 a!3 a!4 a!5 a!6 a!7 a!8)\n (and a!1 a!2 a!3 a!4 a!5 a!6 a!7 a!8))))\n")
% 5.81/300.07 RuntimeError("Could not parse (declare-sort tptp.'Tree' 0)\n(declare-fun tptp.searchtree (|tptp.'Tree'|) Bool)\n(declare-fun |tptp.'right:(Tree)>Tree'| (|tptp.'Tree'|) |tptp.'Tree'|)\n(declare-fun |tptp.'val:(Tree)>Int'| (|tptp.'Tree'|) Int)\n(declare-fun |tptp.'left:(Tree)>Tree'| (|tptp.'Tree'|) |tptp.'Tree'|)\n(declare-fun |tptp.'empty:Tree'| () |tptp.'Tree'|)\n(declare-fun tptp.in (Int |tptp.'Tree'|) Bool)\n(declare-fun |tptp.'node:(Int*Tree*Tree)>Tree'|\n (Int |tptp.'Tree'| |tptp.'Tree'|)\n |tptp.'Tree'|)\n(assert (let ((a!1 (forall ((X |tptp.'Tree'|))\n (or (= X |tptp.'empty:Tree'|)\n (= X\n (|tptp.'node:(Int*Tree*Tree)>Tree'|\n (|tptp.'val:(Tree)>Int'| X)\n (|tptp.'left:(Tree)>Tree'| X)\n (|tptp.'right:(Tree)>Tree'| X))))))\n (a!2 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'val:(Tree)>Int'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_0)))\n (a!3 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'left:(Tree)>Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_1)))\n (a!4 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'right:(Tree)>Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_2)))\n (a!5 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (not (= |tptp.'empty:Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2)))))\n (a!6 (forall ((V Int) (T |tptp.'Tree'|))\n (let ((a!1 (=> (not (= T |tptp.'empty:Tree'|))\n (or (= V (|tptp.'val:(Tree)>Int'| T))\n (tptp.in V (|tptp.'left:(Tree)>Tree'| T))\n (tptp.in V (|tptp.'right:(Tree)>Tree'| T))))))\n (= (tptp.in V T) (and (=> (= T |tptp.'empty:Tree'|) false) a!1)))))\n (a!7 (forall ((T |tptp.'Tree'|))\n (let ((a!1 (forall ((V Int))\n (=> (tptp.in V (|tptp.'left:(Tree)>Tree'| T))\n (<= V (|tptp.'val:(Tree)>Int'| T)))))\n (a!2 (forall ((V Int))\n (=> (tptp.in V (|tptp.'right:(Tree)>Tree'| T))\n (> V (|tptp.'val:(Tree)>Int'| T))))))\n (let ((a!3 (=> (not (= T |tptp.'empty:Tree'|))\n (and (tptp.searchtree (|tptp.'left:(Tree)>Tree'| T))\n (tptp.searchtree (|tptp.'right:(Tree)>Tree'| T))\n a!1\n a!2))))\n (= (tptp.searchtree T)\n (and (=> (= T |tptp.'empty:Tree'|) true) a!3))))))\n (a!8 (not (forall ((T |tptp.'Tree'|) (V Int))\n (let ((a!1 (exists ((T_1 |tptp.'Tree'|))\n (and (= T_1 (|tptp.'left:(Tree)>Tree'| T))\n (tptp.searchtree T_1))))\n (a!2 (exists ((T_2 |tptp.'Tree'|))\n (and (= T_2 (|tptp.'right:(Tree)>Tree'| T))\n (tptp.searchtree T_2)))))\n (let ((a!3 (=> (not (< V (|tptp.'val:(Tree)>Int'| T))) a!2)))\n (let ((a!4 (and (=> (< V (|tptp.'val:(Tree)>Int'| T)) a!1)\n a!3)))\n (let ((a!5 (=> (not (= V (|tptp.'val:(Tree)>Int'| T))) a!4)))\n (let ((a!6 (and (=> (= V (|tptp.'val:(Tree)>Int'| T)) true)\n a!5)))\n (let ((a!7 (and (=> (= T |tptp.'empty:Tree'|) true)\n (=> (not (= T |tptp.'empty:Tree'|)) a!6))))\n (=> (tptp.searchtree T) a!7)))))))))))\n (= (and a!1 a!2 a!3 a!4 a!5 a!6 a!7 a!8)\n (and a!1 a!2 a!3 a!4 a!5 a!6 a!7 a!8))))\n")
% 5.81/300.07 RuntimeError("Could not parse (declare-sort tptp.'Tree' 0)\n(declare-fun tptp.searchtree (|tptp.'Tree'|) Bool)\n(declare-fun |tptp.'right:(Tree)>Tree'| (|tptp.'Tree'|) |tptp.'Tree'|)\n(declare-fun |tptp.'val:(Tree)>Int'| (|tptp.'Tree'|) Int)\n(declare-fun |tptp.'left:(Tree)>Tree'| (|tptp.'Tree'|) |tptp.'Tree'|)\n(declare-fun |tptp.'empty:Tree'| () |tptp.'Tree'|)\n(declare-fun tptp.in (Int |tptp.'Tree'|) Bool)\n(declare-fun |tptp.'node:(Int*Tree*Tree)>Tree'|\n (Int |tptp.'Tree'| |tptp.'Tree'|)\n |tptp.'Tree'|)\n(assert (let ((a!1 (forall ((X |tptp.'Tree'|))\n (or (= X |tptp.'empty:Tree'|)\n (= X\n (|tptp.'node:(Int*Tree*Tree)>Tree'|\n (|tptp.'val:(Tree)>Int'| X)\n (|tptp.'left:(Tree)>Tree'| X)\n (|tptp.'right:(Tree)>Tree'| X))))))\n (a!2 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'val:(Tree)>Int'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_0)))\n (a!3 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'left:(Tree)>Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_1)))\n (a!4 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'right:(Tree)>Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_2)))\n (a!5 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (not (= |tptp.'empty:Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2)))))\n (a!6 (forall ((V Int) (T |tptp.'Tree'|))\n (let ((a!1 (=> (not (= T |tptp.'empty:Tree'|))\n (or (= V (|tptp.'val:(Tree)>Int'| T))\n (tptp.in V (|tptp.'left:(Tree)>Tree'| T))\n (tptp.in V (|tptp.'right:(Tree)>Tree'| T))))))\n (= (tptp.in V T) (and (=> (= T |tptp.'empty:Tree'|) false) a!1)))))\n (a!7 (forall ((T |tptp.'Tree'|))\n (let ((a!1 (forall ((V Int))\n (=> (tptp.in V (|tptp.'left:(Tree)>Tree'| T))\n (<= V (|tptp.'val:(Tree)>Int'| T)))))\n (a!2 (forall ((V Int))\n (=> (tptp.in V (|tptp.'right:(Tree)>Tree'| T))\n (> V (|tptp.'val:(Tree)>Int'| T))))))\n (let ((a!3 (=> (not (= T |tptp.'empty:Tree'|))\n (and (tptp.searchtree (|tptp.'left:(Tree)>Tree'| T))\n (tptp.searchtree (|tptp.'right:(Tree)>Tree'| T))\n a!1\n a!2))))\n (= (tptp.searchtree T)\n (and (=> (= T |tptp.'empty:Tree'|) true) a!3))))))\n (a!8 (not (forall ((T |tptp.'Tree'|) (V Int))\n (let ((a!1 (exists ((T_1 |tptp.'Tree'|))\n (and (= T_1 (|tptp.'left:(Tree)>Tree'| T))\n (tptp.searchtree T_1))))\n (a!2 (exists ((T_2 |tptp.'Tree'|))\n (and (= T_2 (|tptp.'right:(Tree)>Tree'| T))\n (tptp.searchtree T_2)))))\n (let ((a!3 (=> (not (< V (|tptp.'val:(Tree)>Int'| T))) a!2)))\n (let ((a!4 (and (=> (< V (|tptp.'val:(Tree)>Int'| T)) a!1)\n a!3)))\n (let ((a!5 (=> (not (= V (|tptp.'val:(Tree)>Int'| T))) a!4)))\n (let ((a!6 (and (=> (= V (|tptp.'val:(Tree)>Int'| T)) true)\n a!5)))\n (let ((a!7 (and (=> (= T |tptp.'empty:Tree'|) true)\n (=> (not (= T |tptp.'empty:Tree'|)) a!6))))\n (=> (tptp.searchtree T) a!7)))))))))))\n (= (and a!1 a!2 a!3 a!4 a!5 a!6 a!7 a!8)\n (and a!1 a!2 a!3 a!4 a!5 a!6 a!7 a!8))))\n")
% 5.81/300.07 RuntimeError("Could not parse (declare-sort tptp.'Tree' 0)\n(declare-fun tptp.searchtree (|tptp.'Tree'|) Bool)\n(declare-fun |tptp.'right:(Tree)>Tree'| (|tptp.'Tree'|) |tptp.'Tree'|)\n(declare-fun |tptp.'val:(Tree)>Int'| (|tptp.'Tree'|) Int)\n(declare-fun |tptp.'left:(Tree)>Tree'| (|tptp.'Tree'|) |tptp.'Tree'|)\n(declare-fun |tptp.'empty:Tree'| () |tptp.'Tree'|)\n(declare-fun tptp.in (Int |tptp.'Tree'|) Bool)\n(declare-fun |tptp.'node:(Int*Tree*Tree)>Tree'|\n (Int |tptp.'Tree'| |tptp.'Tree'|)\n |tptp.'Tree'|)\n(assert (let ((a!1 (forall ((X |tptp.'Tree'|))\n (or (= X |tptp.'empty:Tree'|)\n (= X\n (|tptp.'node:(Int*Tree*Tree)>Tree'|\n (|tptp.'val:(Tree)>Int'| X)\n (|tptp.'left:(Tree)>Tree'| X)\n (|tptp.'right:(Tree)>Tree'| X))))))\n (a!2 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'val:(Tree)>Int'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_0)))\n (a!3 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'left:(Tree)>Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_1)))\n (a!4 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'right:(Tree)>Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_2)))\n (a!5 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (not (= |tptp.'empty:Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2)))))\n (a!6 (forall ((V Int) (T |tptp.'Tree'|))\n (let ((a!1 (=> (not (= T |tptp.'empty:Tree'|))\n (or (= V (|tptp.'val:(Tree)>Int'| T))\n (tptp.in V (|tptp.'left:(Tree)>Tree'| T))\n (tptp.in V (|tptp.'right:(Tree)>Tree'| T))))))\n (= (tptp.in V T) (and (=> (= T |tptp.'empty:Tree'|) false) a!1)))))\n (a!7 (forall ((T |tptp.'Tree'|))\n (let ((a!1 (forall ((V Int))\n (=> (tptp.in V (|tptp.'left:(Tree)>Tree'| T))\n (<= V (|tptp.'val:(Tree)>Int'| T)))))\n (a!2 (forall ((V Int))\n (=> (tptp.in V (|tptp.'right:(Tree)>Tree'| T))\n (> V (|tptp.'val:(Tree)>Int'| T))))))\n (let ((a!3 (=> (not (= T |tptp.'empty:Tree'|))\n (and (tptp.searchtree (|tptp.'left:(Tree)>Tree'| T))\n (tptp.searchtree (|tptp.'right:(Tree)>Tree'| T))\n a!1\n a!2))))\n (= (tptp.searchtree T)\n (and (=> (= T |tptp.'empty:Tree'|) true) a!3))))))\n (a!8 (not (forall ((T |tptp.'Tree'|) (V Int))\n (let ((a!1 (exists ((T_1 |tptp.'Tree'|))\n (and (= T_1 (|tptp.'left:(Tree)>Tree'| T))\n (tptp.searchtree T_1))))\n (a!2 (exists ((T_2 |tptp.'Tree'|))\n (and (= T_2 (|tptp.'right:(Tree)>Tree'| T))\n (tptp.searchtree T_2)))))\n (let ((a!3 (=> (not (< V (|tptp.'val:(Tree)>Int'| T))) a!2)))\n (let ((a!4 (and (=> (< V (|tptp.'val:(Tree)>Int'| T)) a!1)\n a!3)))\n (let ((a!5 (=> (not (= V (|tptp.'val:(Tree)>Int'| T))) a!4)))\n (let ((a!6 (and (=> (= V (|tptp.'val:(Tree)>Int'| T)) true)\n a!5)))\n (let ((a!7 (and (=> (= T |tptp.'empty:Tree'|) true)\n (=> (not (= T |tptp.'empty:Tree'|)) a!6))))\n (=> (tptp.searchtree T) a!7)))))))))))\n (= (and a!1 a!2 a!3 a!4 a!5 a!6 a!7 a!8)\n (and a!1 a!2 a!3 a!4 a!5 a!6 a!7 a!8))))\n")
% 5.81/300.07 RuntimeError("Could not parse (declare-sort tptp.'Tree' 0)\n(declare-fun tptp.searchtree (|tptp.'Tree'|) Bool)\n(declare-fun |tptp.'right:(Tree)>Tree'| (|tptp.'Tree'|) |tptp.'Tree'|)\n(declare-fun |tptp.'val:(Tree)>Int'| (|tptp.'Tree'|) Int)\n(declare-fun |tptp.'left:(Tree)>Tree'| (|tptp.'Tree'|) |tptp.'Tree'|)\n(declare-fun |tptp.'empty:Tree'| () |tptp.'Tree'|)\n(declare-fun tptp.in (Int |tptp.'Tree'|) Bool)\n(declare-fun |tptp.'node:(Int*Tree*Tree)>Tree'|\n (Int |tptp.'Tree'| |tptp.'Tree'|)\n |tptp.'Tree'|)\n(assert (let ((a!1 (forall ((X |tptp.'Tree'|))\n (or (= X |tptp.'empty:Tree'|)\n (= X\n (|tptp.'node:(Int*Tree*Tree)>Tree'|\n (|tptp.'val:(Tree)>Int'| X)\n (|tptp.'left:(Tree)>Tree'| X)\n (|tptp.'right:(Tree)>Tree'| X))))))\n (a!2 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'val:(Tree)>Int'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_0)))\n (a!3 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'left:(Tree)>Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_1)))\n (a!4 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (= (|tptp.'right:(Tree)>Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2))\n X_1_2)))\n (a!5 (forall ((X_1_0 Int) (X_1_1 |tptp.'Tree'|) (X_1_2 |tptp.'Tree'|))\n (not (= |tptp.'empty:Tree'|\n (|tptp.'node:(Int*Tree*Tree)>Tree'| X_1_0 X_1_1 X_1_2)))))\n (a!6 (forall ((V Int) (T |tptp.'Tree'|))\n (let ((a!1 (=> (not (= T |tptp.'empty:Tree'|))\n (or (= V (|tptp.'val:(Tree)>Int'| T))\n (tptp.in V (|tptp.'left:(Tree)>Tree'| T))\n (tptp.in V (|tptp.'right:(Tree)>Tree'| T))))))\n (= (tptp.in V T) (and (=> (= T |tptp.'empty:Tree'|) false) a!1)))))\n (a!7 (forall ((T |tptp.'Tree'|))\n (let ((a!1 (forall ((V Int))\n (=> (tptp.in V (|tptp.'left:(Tree)>Tree'| T))\n (<= V (|tptp.'val:(Tree)>Int'| T)))))\n (a!2 (forall ((V Int))\n (=> (tptp.in V (|tptp.'right:(Tree)>Tree'| T))\n (> V (|tptp.'val:(Tree)>Int'| T))))))\n (let ((a!3 (=> (not (= T |tptp.'empty:Tree'|))\n (and (tptp.searchtree (|tptp.'left:(Tree)>Tree'| T))\n (tptp.searchtree (|tptp.'right:(Tree)>Tree'| T))\n a!1\n a!2))))\n (= (tptp.searchtree T)\n (and (=> (= T |tptp.'empty:Tree'|) true) a!3))))))\n (a!8 (not (forall ((T |tptp.'Tree'|) (V Int))\n (let ((a!1 (exists ((T_1 |tptp.'Tree'|))\n (and (= T_1 (|tptp.'left:(Tree)>Tree'| T))\n (tptp.searchtree T_1))))\n (a!2 (exists ((T_2 |tptp.'Tree'|))\n (and (= T_2 (|tptp.'right:(Tree)>Tree'| T))\n (tptp.searchtree T_2)))))\n (let ((a!3 (=> (not (< V (|tptp.'val:(Tree)>Int'| T))) a!2)))\n (let ((a!4 (and (=> (< V (|tptp.'val:(Tree)>Int'| T)) a!1)\n a!3)))\n (let ((a!5 (=> (not (= V (|tptp.'val:(Tree)>Int'| T))) a!4)))\n (let ((a!6 (and (=> (= V (|tptp.'val:(Tree)>Int'| T)) true)\n a!5)))\n (let ((a!7 (and (=> (= T |tptp.'empty:Tree'|) true)\n (=> (not (= T |tptp.'empty:Tree'|)) a!6))))\n (=> (tptp.searchtree T) a!7)))))))))))\n (= (and a!1 a!2 a!3 a!4 a!5 a!6 a!7 a!8)\n (and a!1 a!2 a!3 a!4 a!5 a!6 a!7 a!8))))\n")% FEST exiting
% 5.81/300.07 % FEST exiting
%------------------------------------------------------------------------------