%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO846+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:32:37 PM UTC 2026
% Result : CounterSatisfiable 0.18s 0.28s
% Output : Saturation 0.18s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u236,axiom,
~ ain(a1,aun(asing(a1),asing(asing(a1)))) ).
cnf(u246,axiom,
~ ain(a1,a0) ).
cnf(u181,axiom,
aun(asing(a2),apow(asing(a2))) = aint(aun(aun(asing(a2),apow(asing(a2))),asing(asm(a3,asing(a1)))),aun(asm(apow(a2),apow(asing(a2))),aun(apow(asing(a2)),asing(apow(a2))))) ).
cnf(u130,axiom,
( ~ aal4(asm(aun(X0,X1),asing(X2)))
| aal3(X1)
| aal3(X0)
| ~ ain(X2,aun(X0,X1)) ) ).
cnf(u191,axiom,
aex3(aun(a2,asing(apow(a2)))) ).
cnf(u219,axiom,
( ~ ain(sK0(aun(asing(a1),asing(asing(a1))),X0),asing(a2))
| asubq(aun(asing(a1),asing(asing(a1))),X0)
| ~ asubq(X0,aun(asing(a1),asing(asing(a1)))) ) ).
cnf(u148,axiom,
ain(asing(a1),aun(asing(asing(a1)),asing(asing(asing(a1))))) ).
cnf(u205,axiom,
( asubq(sK0(apow(X0),X1),X0)
| ~ asubq(X1,apow(X0))
| asubq(apow(X0),X1) ) ).
cnf(u171,axiom,
~ asubq(aun(asing(asing(a1)),aun(asing(asing(a2)),a4)),aun(asing(asing(a2)),a4)) ).
cnf(u128,axiom,
( asubq(X1,asm(X0,asing(sK0(X0,X1))))
| asubq(X0,X1)
| ~ asubq(X1,X0) ) ).
cnf(u189,axiom,
aal4(apow(a2)) ).
cnf(u217,axiom,
( ~ asubq(X0,asm(a4,apow(asing(a2))))
| a3 = sK0(asm(a4,apow(asing(a2))),X0)
| a1 = sK0(asm(a4,apow(asing(a2))),X0)
| asubq(asm(a4,apow(asing(a2))),X0)
| a2 = sK0(asm(a4,apow(asing(a2))),X0) ) ).
cnf(u138,axiom,
asing(asing(a1)) != apow(asing(a1)) ).
cnf(u156,axiom,
ain(a1,asm(aun(asing(asing(a2)),a4),asm(apow(a2),asing(a1)))) ).
cnf(u166,axiom,
( ~ ain(X0,asm(a4,asing(a1)))
| a2 = X0
| a3 = X0
| a0 = X0 ) ).
cnf(u194,axiom,
asubq(asm(aint(aun(aun(asing(a1),asing(asing(a1))),aun(apow(asing(a2)),asing(a3))),aun(asing(asing(a2)),a4)),asing(a0)),asm(aun(asing(asing(a2)),a4),asm(apow(a2),asing(a1)))) ).
cnf(u255,axiom,
( asubq(asm(a4,apow(asing(a2))),sK0(apow(asm(a4,apow(asing(a2)))),X0))
| a1 = sK0(asm(a4,apow(asing(a2))),sK0(apow(asm(a4,apow(asing(a2)))),X0))
| a3 = sK0(asm(a4,apow(asing(a2))),sK0(apow(asm(a4,apow(asing(a2)))),X0))
| a2 = sK0(asm(a4,apow(asing(a2))),sK0(apow(asm(a4,apow(asing(a2)))),X0))
| ~ asubq(X0,apow(asm(a4,apow(asing(a2)))))
| asubq(apow(asm(a4,apow(asing(a2)))),X0) ) ).
cnf(u168,axiom,
~ asubq(aun(asing(apow(asing(a1))),a4),a4) ).
cnf(u212,axiom,
( ~ ain(sK0(asm(a3,asing(a1)),X0),asing(a3))
| asubq(asm(a3,asing(a1)),X0)
| ~ asubq(X0,asm(a3,asing(a1))) ) ).
cnf(u129,axiom,
( ain(sK0(X0,X1),X0)
| asubq(X0,X1)
| ~ asubq(X1,X0) ) ).
cnf(u178,axiom,
asm(a3,asing(a1)) = asm(asm(a4,asing(a1)),asing(a3)) ).
cnf(u192,axiom,
( ~ aal3(asm(aint(aun(a3,asing(asm(a3,asing(a1)))),apow(asm(a3,asing(a1)))),asing(X0)))
| ~ ain(X0,apow(asm(a3,asing(a1))))
| ~ ain(X0,a3) ) ).
cnf(u253,axiom,
( asubq(asm(a4,asing(a1)),sK0(apow(asm(a4,asing(a1))),X0))
| a0 = sK0(asm(a4,asing(a1)),sK0(apow(asm(a4,asing(a1))),X0))
| a3 = sK0(asm(a4,asing(a1)),sK0(apow(asm(a4,asing(a1))),X0))
| a2 = sK0(asm(a4,asing(a1)),sK0(apow(asm(a4,asing(a1))),X0))
| ~ asubq(X0,apow(asm(a4,asing(a1))))
| asubq(apow(asm(a4,asing(a1))),X0) ) ).
cnf(u174,axiom,
asubq(asm(asm(apow(a2),a2),asing(asing(a1))),asing(a2)) ).
cnf(u202,axiom,
asubq(a0,apow(asing(a1))) ).
cnf(u135,axiom,
~ ain(asing(asing(a1)),a2) ).
cnf(u176,axiom,
aun(asing(a1),asing(asing(a1))) = asm(asm(apow(a2),apow(asing(a2))),asing(a2)) ).
cnf(u137,axiom,
a2 != apow(asing(a1)) ).
cnf(u186,axiom,
aal3(asm(apow(aun(asing(a1),asing(asing(a1)))),asing(aun(asing(a1),asing(asing(a1)))))) ).
cnf(u119,axiom,
( ~ aal4(X0)
| ~ aex3(X0) ) ).
cnf(u147,axiom,
~ ain(asing(asing(a1)),asing(apow(asing(a1)))) ).
cnf(u121,axiom,
( ~ ain(X0,a3)
| a1 = X0
| a2 = X0
| a0 = X0 ) ).
cnf(u165,axiom,
( ~ ain(X0,aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1)))))
| a1 = X0
| asing(a1) = X0
| asing(asing(a1)) = X0
| a0 = X0 ) ).
cnf(u193,axiom,
~ aal3(asm(aint(aun(a3,asing(asm(a3,asing(a1)))),apow(asm(a3,asing(a1)))),asing(asm(a3,asing(a1))))) ).
cnf(u175,axiom,
asubq(asm(asm(apow(a2),a2),asing(a2)),asing(asing(a1))) ).
cnf(u203,axiom,
~ ain(a2,asing(a1)) ).
cnf(u132,axiom,
~ ain(a2,a2) ).
cnf(u177,axiom,
asubq(aun(asing(a1),asing(a3)),asm(asm(a4,asing(a2)),asing(a0))) ).
cnf(u155,axiom,
~ ain(a1,aun(asing(asing(a1)),asing(a3))) ).
cnf(u173,axiom,
asubq(a2,asm(a3,asing(a2))) ).
cnf(u201,axiom,
asubq(a0,asing(asing(a1))) ).
cnf(u250,axiom,
( ~ ain(sK0(aun(asing(a2),aun(apow(asing(a2)),asing(apow(a2)))),X0),aun(apow(a2),asing(asing(a2))))
| ~ ain(sK0(aun(asing(a2),aun(apow(asing(a2)),asing(apow(a2)))),X0),asing(apow(a2)))
| asubq(aun(asing(a2),aun(apow(asing(a2)),asing(apow(a2)))),X0)
| ~ asubq(X0,aun(asing(a2),aun(apow(asing(a2)),asing(apow(a2))))) ) ).
cnf(u183,axiom,
( ~ aal2(asm(a2,asing(X0)))
| ~ ain(X0,a2) ) ).
cnf(u211,axiom,
( ~ ain(X0,asm(a3,asing(a1)))
| ~ ain(X0,asing(a3)) ) ).
cnf(u140,axiom,
~ ain(asm(apow(a2),apow(asing(a2))),asm(apow(a2),asing(a2))) ).
cnf(u185,axiom,
aal2(asm(a4,a2)) ).
cnf(u150,axiom,
ain(asing(asing(a1)),aun(asm(apow(a2),a2),apow(asing(asing(a1))))) ).
cnf(u152,axiom,
ain(a2,asm(a4,asing(a1))) ).
cnf(u196,axiom,
ain(a1,a3) ).
cnf(u162,axiom,
ain(a2,aun(asm(apow(a2),apow(asing(a2))),aun(apow(asing(a2)),asing(apow(a2))))) ).
cnf(u180,axiom,
( ~ ain(X0,aun(asing(a2),aun(apow(asing(a2)),asing(apow(a2)))))
| ~ ain(X0,asing(apow(a2)))
| ~ ain(X0,aun(apow(a2),asing(asing(a2)))) ) ).
cnf(u125,axiom,
( ~ ain(X1,apow(X0))
| asubq(X1,X0) ) ).
cnf(u158,axiom,
ain(a2,aun(asing(asing(a1)),aun(asing(asing(a2)),a4))) ).
cnf(u160,axiom,
~ ain(asm(a3,asing(a1)),aun(apow(asing(a2)),asing(apow(a2)))) ).
cnf(u204,axiom,
asubq(a0,aun(asing(a1),asing(asing(a1)))) ).
cnf(u249,axiom,
( asubq(a3,sK0(apow(a3),X0))
| a0 = sK0(a3,sK0(apow(a3),X0))
| a2 = sK0(a3,sK0(apow(a3),X0))
| a1 = sK0(a3,sK0(apow(a3),X0))
| ~ asubq(X0,apow(a3))
| asubq(apow(a3),X0) ) ).
cnf(u170,axiom,
asubq(apow(a2),aun(asing(asing(a1)),aun(a4,asing(apow(a2))))) ).
cnf(u214,axiom,
~ aex3(aun(asm(apow(a2),asing(a2)),asing(asm(apow(a2),apow(asing(a2)))))) ).
cnf(u131,axiom,
~ ain(a0,a0) ).
cnf(u188,axiom,
aal3(aun(a2,asing(apow(a2)))) ).
cnf(u216,axiom,
( ~ asubq(X0,asm(a4,asing(a1)))
| a3 = sK0(asm(a4,asing(a1)),X0)
| a0 = sK0(asm(a4,asing(a1)),X0)
| asubq(asm(a4,asing(a1)),X0)
| a2 = sK0(asm(a4,asing(a1)),X0) ) ).
cnf(u149,axiom,
ain(a0,apow(aun(asing(a1),asing(asing(a1))))) ).
cnf(u159,axiom,
~ ain(asm(apow(a2),a2),aun(asing(asing(a1)),aun(asing(asing(a2)),a4))) ).
cnf(u161,axiom,
ain(a1,aun(asm(apow(a2),apow(asing(a1))),aun(asing(asing(a2)),asing(apow(a2))))) ).
cnf(u139,axiom,
asubq(aun(asing(a1),asing(asing(a1))),asm(apow(a2),asing(a2))) ).
cnf(u224,axiom,
( ain(asing(a1),sK0(apow(aun(asing(a1),asing(asing(a1)))),X0))
| ~ ain(a1,sK0(apow(aun(asing(a1),asing(asing(a1)))),X0))
| asing(a1) = sK0(apow(aun(asing(a1),asing(asing(a1)))),X0)
| ~ asubq(X0,apow(aun(asing(a1),asing(asing(a1)))))
| asubq(apow(aun(asing(a1),asing(asing(a1)))),X0) ) ).
cnf(u157,axiom,
~ ain(asing(a1),aun(asing(asing(a2)),a4)) ).
cnf(u167,axiom,
( ~ ain(X0,asm(a4,apow(asing(a2))))
| a2 = X0
| a3 = X0
| a1 = X0 ) ).
cnf(u195,axiom,
ain(a0,a3) ).
cnf(u169,axiom,
~ asubq(aun(asm(apow(a2),apow(asing(a2))),apow(asing(asing(a1)))),aun(asm(apow(a2),apow(asing(a1))),apow(asing(asing(a1))))) ).
cnf(u213,axiom,
~ ain(a1,asm(apow(a2),asing(a1))) ).
cnf(u134,axiom,
a0 != asing(a1) ).
cnf(u179,axiom,
a3 = aint(aun(apow(a2),asing(asing(a2))),aun(a4,asing(asm(apow(a2),a2)))) ).
cnf(u257,axiom,
( asubq(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1)))),sK0(apow(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1))))),X0))
| asing(asing(a1)) = sK0(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1)))),sK0(apow(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1))))),X0))
| a0 = sK0(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1)))),sK0(apow(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1))))),X0))
| asing(a1) = sK0(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1)))),sK0(apow(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1))))),X0))
| a1 = sK0(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1)))),sK0(apow(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1))))),X0))
| ~ asubq(X0,apow(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1))))))
| asubq(apow(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1))))),X0) ) ).
cnf(u136,axiom,
~ ain(asm(a3,asing(a1)),a2) ).
cnf(u146,axiom,
ain(a0,apow(apow(asing(a1)))) ).
cnf(u120,axiom,
( ~ aex3(X0)
| aal3(X0) ) ).
cnf(u164,axiom,
( ~ asubq(X0,aun(asing(a1),asing(asing(a1))))
| ~ ain(a1,X0)
| ain(asing(a1),X0)
| asing(a1) = X0 ) ).
cnf(u142,axiom,
~ ain(asm(apow(a2),apow(asing(a2))),asm(apow(a2),asing(a1))) ).
cnf(u187,axiom,
aal3(asm(a4,asing(a2))) ).
cnf(u144,axiom,
ain(asing(asing(a1)),asing(asing(asing(a1)))) ).
cnf(u126,axiom,
( ~ ain(X2,asm(X0,X1))
| ~ ain(X2,X1) ) ).
cnf(u154,axiom,
~ ain(asm(apow(a2),a2),a4) ).
cnf(u198,axiom,
~ aex3(apow(a2)) ).
cnf(u172,axiom,
asubq(a1,asm(a2,asing(a1))) ).
cnf(u200,axiom,
asubq(X0,X0) ).
cnf(u133,axiom,
~ asubq(a2,a0) ).
cnf(u182,axiom,
~ aal2(asing(a3)) ).
cnf(u210,axiom,
( ~ asubq(X0,a3)
| a2 = sK0(a3,X0)
| a0 = sK0(a3,X0)
| asubq(a3,X0)
| a1 = sK0(a3,X0) ) ).
cnf(u143,axiom,
apow(a2) != asm(apow(a2),apow(asing(a2))) ).
cnf(u184,axiom,
( ~ aal3(asm(aun(apow(asing(a2)),asing(apow(a2))),asing(X0)))
| ~ ain(X0,aun(apow(asing(a2)),asing(apow(a2)))) ) ).
cnf(u145,axiom,
ain(a0,apow(asing(asing(a1)))) ).
cnf(u127,axiom,
ain(X0,apow(X0)) ).
cnf(u206,axiom,
( ~ ain(sK0(asm(X0,X1),X2),X1)
| ~ asubq(X2,asm(X0,X1))
| asubq(asm(X0,X1),X2) ) ).
cnf(u251,axiom,
( ~ asubq(X0,aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1)))))
| asing(a1) = sK0(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1)))),X0)
| asing(asing(a1)) = sK0(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1)))),X0)
| a0 = sK0(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1)))),X0)
| asubq(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1)))),X0)
| a1 = sK0(aun(aun(asing(a1),asing(asing(a1))),apow(asing(asing(a1)))),X0) ) ).
cnf(u141,axiom,
a2 != asing(a2) ).
cnf(u190,axiom,
aal4(aun(asm(apow(a2),asing(a2)),asing(asm(apow(a2),apow(asing(a2)))))) ).
cnf(u218,axiom,
( ~ ain(X0,aun(asing(a1),asing(asing(a1))))
| ~ ain(X0,asing(a2)) ) ).
cnf(u151,axiom,
ain(a1,aun(asm(apow(a2),apow(asing(a2))),asing(asing(asing(a1))))) ).
cnf(u153,axiom,
~ ain(a1,asing(a3)) ).
cnf(u197,axiom,
ain(a2,a3) ).
cnf(u163,axiom,
ain(a1,aun(asing(asing(a1)),aun(a4,asing(apow(a2))))) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO846+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n026.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 18:37:57 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.28 % (4119327)Will run a generic schedule for satisfiability detection.
% 0.18/0.28 % (4119341)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=537089287:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.28 % (4119337)% WARNING: option uhcvi not known.
% 0.18/0.28 % (4119339)dis+10_1_sil=32000:sp=arity:random_seed=1988165409:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.28 % (4119336)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=729988291_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.28 % (4119338)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2178755727:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.28 % (4119337)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2474388509:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.28 % (4119343)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2048821940:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.28 % (4119342)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1149844656:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.28 % TRYING [1]
% 0.18/0.28 % TRYING [2]
% 0.18/0.28 % (4119339) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4119327-4119339"...
% 0.18/0.28 % TRYING [3]
% 0.18/0.28 % (4119342) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4119327-4119342"...
% 0.18/0.28 % (4119337) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4119327-4119337"...
% 0.18/0.28 % (4119343) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4119327-4119343"...
% 0.18/0.28 % (4119339)...printing done.
% 0.18/0.28 % SZS status CounterSatisfiable for theBenchmark
% 0.18/0.28 % SZS output start Saturation.
% See solution above
% 0.18/0.28 % SZS output start Definitions and Model Updates.
% 0.18/0.28 for all inputs,
% 0.18/0.28 define aal6(X0) := $false
% 0.18/0.28 for all inputs,
% 0.18/0.28 define aal7(X0) := $false
% 0.18/0.28 for all inputs,
% 0.18/0.28 define aex2(X0) := $true
% 0.18/0.28 for all inputs,
% 0.18/0.28 define aex5(X0) := $true
% 0.18/0.28 for all inputs,
% 0.18/0.28 define aex4(X0) := $false
% 0.18/0.28 for all inputs,
% 0.18/0.28 define aal5(X0) := $true
% 0.18/0.28 for all groundings,
% 0.18/0.28 whenever ? [X1] : (asubq(X1,X0) & ~asubq(X0,X1) & aal5(X1)) is true, set aal6(X0) to true
% 0.18/0.28 for all groundings,
% 0.18/0.28 whenever aal3(X0) & ~aal4(X0) is true, set aex3(X0) to true
% 0.18/0.28 % SZS output end Definitions and Model Updates.
% 0.18/0.28 % (4119339)------------------------------
% 0.18/0.28 % (4119339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.28 % (4119339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.28 % (4119339)CaDiCaL version: 2.1.3
% 0.18/0.28 % (4119339)Termination reason: Satisfiable
% 0.18/0.28 % (4119339)Time elapsed: 0.010 s
% 0.18/0.28 % (4119339)Peak memory usage: 12 MB
% 0.18/0.28 % (4119339)Instructions burned: 14 (million)
% 0.18/0.28 % (4119327)Success in time 0.045 s
% 0.18/0.28 % Vampire exiting
%------------------------------------------------------------------------------