%------------------------------------------------------------------------------
% File : FEST---2.0.1
% Problem : DAT331_1 : TPTP v9.0.0. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fest %s %d
% Computer : n014.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:34:00 AM UTC 2025
% Result : Timeout 4.30s 300.08s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : DAT331_1 : TPTP v9.0.0. Released v7.0.0.
% 0.06/0.11 % Command : run_fest %s %d
% 0.11/0.32 % Computer : n014.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Fri Mar 28 18:40:34 EDT 2025
% 0.11/0.32 % CPUTime :
% 4.30/300.08 Alarm clock
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")
% 4.30/300.08 RuntimeError("Could not parse (declare-sort |tptp.'Array[Int,Int]'| 0)\n(declare-sort tptp.'Set' 0)\n(declare-fun |tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'Array[Int,Int]'| Int)\n Int)\n(declare-fun |tptp.'const:(Int)>Array[Int,Int]'| (Int) |tptp.'Array[Int,Int]'|)\n(declare-fun |tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n (|tptp.'Array[Int,Int]'| Int Int)\n |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.sup (|tptp.'Set'|) Int)\n(declare-fun tptp.s0 () |tptp.'Set'|)\n(declare-fun tptp.s4 () |tptp.'Set'|)\n(declare-fun tptp.insert (|tptp.'Set'| Int) |tptp.'Set'|)\n(declare-fun tptp.i4 () Int)\n(declare-fun tptp.s3 () |tptp.'Set'|)\n(declare-fun tptp.g (Int) Int)\n(declare-fun tptp.i3 () Int)\n(declare-fun tptp.arr () |tptp.'Array[Int,Int]'|)\n(declare-fun tptp.s2 () |tptp.'Set'|)\n(declare-fun tptp.i2 () Int)\n(declare-fun tptp.s1 () |tptp.'Set'|)\n(declare-fun tptp.i1 () Int)\n(declare-fun tptp.member (Int |tptp.'Set'|) Bool)\n(declare-fun tptp.delete (|tptp.'Set'| Int) |tptp.'Set'|)\n(assert (let ((a!1 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_y))\n (tptp.member A__questionmark_x A__questionmark_s)))))\n (a!2 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (=> (not (tptp.member A__questionmark_x A__questionmark_s))\n (= (tptp.delete A__questionmark_s A__questionmark_x)\n A__questionmark_s))))\n (a!3 (forall ((A__questionmark_x Int) (A__questionmark_s |tptp.'Set'|))\n (= (tptp.delete (tptp.insert A__questionmark_s A__questionmark_x)\n A__questionmark_x)\n (tptp.delete A__questionmark_s A__questionmark_x))))\n (a!4 (forall ((A__questionmark_x Int)\n (A__questionmark_y Int)\n (A__questionmark_s |tptp.'Set'|))\n (=> (not (= A__questionmark_x A__questionmark_y))\n (= (tptp.delete (tptp.insert A__questionmark_s\n A__questionmark_y)\n A__questionmark_x)\n (tptp.insert (tptp.delete A__questionmark_s\n A__questionmark_x)\n A__questionmark_y)))))\n (a!5 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (tptp.member A__questionmark_x A__questionmark_s)\n (<= A__questionmark_x (tptp.sup A__questionmark_s)))))\n (a!6 (forall ((A__questionmark_s |tptp.'Set'|) (A__questionmark_x Int))\n (=> (< (tptp.sup A__questionmark_s) A__questionmark_x)\n (= (tptp.sup (tptp.insert A__questionmark_s A__questionmark_x))\n A__questionmark_x))))\n (a!7 (forall ((A__questionmark_i Int))\n (=> (> A__questionmark_i 0)\n (< (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n A__questionmark_i)\n (tptp.sup tptp.s0)))))\n (a!8 (=> (> tptp.i1 0)\n (= tptp.s1\n (tptp.insert tptp.s0\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n tptp.i1)))))\n (a!9 (= tptp.s2\n (tptp.insert tptp.s1\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i2)))))\n (a!10 (= tptp.s3\n (tptp.insert tptp.s2\n (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n tptp.arr\n (tptp.g tptp.i3)))))\n (a!11 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n I)\n E)))\n (a!12 (forall ((A |tptp.'Array[Int,Int]'|) (I Int) (J Int) (E Int))\n (=> (not (= I J))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'|\n A\n I\n E)\n J)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| A J)))))\n (a!13 (forall ((A |tptp.'Array[Int,Int]'|) (B |tptp.'Array[Int,Int]'|))\n (=> (forall ((I Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'| A I)\n (|tptp.'select:(Array[Int,Int]*Int)>Int'| B I)))\n (= A B))))\n (a!14 (forall ((I Int) (E Int))\n (= (|tptp.'select:(Array[Int,Int]*Int)>Int'|\n (|tptp.'const:(Int)>Array[Int,Int]'| E)\n I)\n E))))\n(let ((a!15 (and (forall ((A__questionmark_x Int)\n (A__questionmark_s |tptp.'Set'|))\n (tptp.member A__questionmark_x\n (tptp.insert A__questionmark_s\n A__questionmark_x)))\n a!1\n a!2\n a!3\n a!4\n (forall ((A__questionmark_s |tptp.'Set'|))\n (tptp.member (tptp.sup A__questionmark_s) A__questionmark_s))\n a!5\n a!6\n a!7\n (forall ((A__questionmark_i Int))\n (> (tptp.g A__questionmark_i) 0))\n a!8\n (=> (not (> tptp.i1 0)) (= tptp.s1 tptp.s0))\n a!9\n a!10\n (= tptp.s4 (tptp.insert tptp.s3 tptp.i4))\n (not (= (tptp.sup tptp.s4) (tptp.sup tptp.s0)))\n a!11\n a!12\n a!13\n a!14)))\n (= a!15 a!15))))\n")% FEST exiting
% 4.30/300.08 % FEST exiting
%------------------------------------------------------------------------------