%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR143^2 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 07:47:20 AM UTC 2026
% Result : Theorem 101.15s 14.56s
% Output : Refutation 101.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR143^2 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.19 % Computer : n007.cluster.edu
% 0.11/0.19 % Model : x86_64 x86_64
% 0.11/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.19 % Memory : 8046.5625MB
% 0.11/0.19 % OS : Linux 6.8.0-71-generic
% 0.11/0.19 % CPULimit : 300
% 0.11/0.19 % WCLimit : 300
% 0.11/0.19 % DateTime : Tue Sep 29 17:54:56 UTC 2026
% 0.11/0.19 % CPUTime :
% 0.11/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.23 Running first-order model finding
% 0.11/0.23 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
% 3.56/0.88 % (3718441)Will run a generic schedule for satisfiability detection.
% 3.56/0.88 % (3718467)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3068618711:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.56/0.88 % (3718462)% WARNING: option uhcvi not known.
% 3.56/0.88 % (3718461)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1774024921_2999 on theBenchmark for (2999ds/0Mi)
% 3.56/0.88 % (3718463)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3084417313:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.56/0.88 % (3718462)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=923298631:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.56/0.88 % (3718464)dis+10_1_sil=32000:sp=arity:random_seed=373403403:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.56/0.88 % (3718465)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1714754565:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.56/0.88 % (3718466)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3594888948:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.56/0.88 % (3718462)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.56/0.88 % (3718465)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.56/0.88 % Exception at run slice level
% 3.56/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.56/0.88 % (3718462)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.56/0.88 % (3718467)Instruction limit reached!
% 3.56/0.88 % (3718467)------------------------------
% 3.56/0.88 % (3718467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.56/0.88 % (3718467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/0.88 % (3718467)CaDiCaL version: 2.1.3
% 3.56/0.88 % (3718467)Termination reason: Instruction limit
% 3.56/0.88 % (3718467)Termination phase: Saturation
% 3.56/0.88 % (3718467)Time elapsed: 0.036 s
% 3.56/0.88 % (3718467)Peak memory usage: 12 MB
% 3.56/0.88 % (3718467)Instructions burned: 160 (million)
% 3.56/0.88 % (3718475)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=530229919:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.56/0.88 % (3718476)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3820263550:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.56/0.88 % (3718464)Instruction limit reached!
% 3.56/0.88 % (3718464)------------------------------
% 3.56/0.88 % (3718464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.56/0.88 % (3718464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/0.88 % (3718464)CaDiCaL version: 2.1.3
% 3.56/0.88 % (3718464)Termination reason: Instruction limit
% 3.56/0.88 % (3718464)Termination phase: Saturation
% 3.56/0.88 % (3718464)Time elapsed: 0.046 s
% 3.56/0.88 % (3718464)Peak memory usage: 12 MB
% 3.56/0.88 % (3718464)Instructions burned: 105 (million)
% 3.56/0.88 % Exception at run slice level
% 3.56/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.56/0.88 % (3718465)Instruction limit reached!
% 3.56/0.88 % (3718465)------------------------------
% 3.56/0.88 % (3718465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.56/0.88 % (3718465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/0.88 % (3718465)CaDiCaL version: 2.1.3
% 3.56/0.88 % (3718465)Termination reason: Instruction limit
% 3.56/0.88 % (3718465)Termination phase: Saturation
% 3.56/0.88 % (3718465)Time elapsed: 0.051 s
% 3.56/0.88 % (3718465)Peak memory usage: 13 MB
% 3.56/0.88 % (3718465)Instructions burned: 118 (million)
% 3.56/0.88 % (3718466)Instruction limit reached!
% 3.56/0.88 % (3718466)------------------------------
% 3.56/0.88 % (3718466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.56/0.88 % (3718466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/0.88 % (3718466)CaDiCaL version: 2.1.3
% 3.56/0.88 % (3718466)Termination reason: Instruction limit
% 3.56/0.88 % (3718466)Termination phase: Saturation
% 3.56/0.88 % (3718466)Time elapsed: 0.057 s
% 3.56/0.88 % (3718466)Peak memory usage: 13 MB
% 3.56/0.88 % (3718466)Instructions burned: 133 (million)
% 3.56/0.88 % (3718479)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3702855877:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 15.28/2.45 % (3718480)ott-21_1_sil=16000:fs=off:random_seed=1572245354:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 15.28/2.45 % (3718481)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2496000499:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 15.28/2.45 % (3718476)Instruction limit reached!
% 15.28/2.45 % (3718476)------------------------------
% 15.28/2.45 % (3718476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.28/2.45 % (3718476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.28/2.45 % (3718476)CaDiCaL version: 2.1.3
% 15.28/2.45 % (3718476)Termination reason: Instruction limit
% 15.28/2.45 % (3718476)Termination phase: Saturation
% 15.28/2.45 % (3718476)Time elapsed: 0.031 s
% 15.28/2.45 % (3718476)Peak memory usage: 13 MB
% 15.28/2.45 % (3718476)Instructions burned: 133 (million)
% 15.28/2.45 % (3718479)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 15.28/2.45 % (3718482)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1075034195:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 15.28/2.45 % (3718479)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 15.28/2.45 % (3718486)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4294253004:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 15.28/2.45 % Exception at run slice level
% 15.28/2.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 15.28/2.45 % (3718492)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3644203708:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 15.28/2.45 % Exception at run slice level
% 15.28/2.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 15.28/2.45 % (3718507)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2972196753:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 15.28/2.45 % (3718480)Instruction limit reached!
% 15.28/2.45 % (3718480)------------------------------
% 15.28/2.45 % (3718480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.28/2.45 % (3718480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.28/2.45 % (3718480)CaDiCaL version: 2.1.3
% 15.28/2.45 % (3718480)Termination reason: Instruction limit
% 15.28/2.45 % (3718480)Termination phase: Saturation
% 15.28/2.45 % (3718480)Time elapsed: 0.075 s
% 15.28/2.45 % (3718480)Peak memory usage: 12 MB
% 15.28/2.45 % (3718480)Instructions burned: 181 (million)
% 15.28/2.45 % (3718507)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 15.28/2.45 % (3718515)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3768846584:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 15.28/2.45 % (3718515)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 15.28/2.45 % (3718481)Instruction limit reached!
% 15.28/2.45 % (3718481)------------------------------
% 15.28/2.45 % (3718481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.28/2.45 % (3718481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.28/2.45 % (3718481)CaDiCaL version: 2.1.3
% 15.28/2.45 % (3718481)Termination reason: Instruction limit
% 15.28/2.45 % (3718481)Termination phase: Saturation
% 15.28/2.45 % (3718481)Time elapsed: 0.209 s
% 15.28/2.45 % (3718481)Peak memory usage: 13 MB
% 15.28/2.45 % (3718481)Instructions burned: 479 (million)
% 15.28/2.45 % (3718565)fmb+10_1_sil=64000:random_seed=2560999987:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 15.28/2.45 % (3718565)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 15.28/2.45 % Exception at run slice level
% 15.28/2.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 15.28/2.45 % (3718573)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=384498759:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 15.28/2.45 % Exception at run slice level
% 15.28/2.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 32.37/4.88 % (3718486)Instruction limit reached!
% 32.37/4.88 % (3718486)------------------------------
% 32.37/4.88 % (3718486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.37/4.88 % (3718486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.37/4.88 % (3718486)CaDiCaL version: 2.1.3
% 32.37/4.88 % (3718486)Termination reason: Instruction limit
% 32.37/4.88 % (3718486)Termination phase: Saturation
% 32.37/4.88 % (3718486)Time elapsed: 0.281 s
% 32.37/4.88 % (3718486)Peak memory usage: 17 MB
% 32.37/4.88 % (3718486)Instructions burned: 1180 (million)
% 32.37/4.88 % (3718584)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1227835537:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 32.37/4.88 % (3718479)Instruction limit reached!
% 32.37/4.88 % (3718479)------------------------------
% 32.37/4.88 % (3718479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.37/4.88 % (3718479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.37/4.88 % (3718479)CaDiCaL version: 2.1.3
% 32.37/4.88 % (3718479)Termination reason: Instruction limit
% 32.37/4.88 % (3718479)Termination phase: Saturation
% 32.37/4.88 % (3718479)Time elapsed: 0.302 s
% 32.37/4.88 % (3718479)Peak memory usage: 13 MB
% 32.37/4.88 % (3718479)Instructions burned: 686 (million)
% 32.37/4.88 % (3718591)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2300523411:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 32.37/4.88 % (3718591)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 32.37/4.88 % Exception at run slice level
% 32.37/4.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 32.37/4.88 % (3718593)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2181168804:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 32.37/4.88 % (3718593)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 32.37/4.88 % (3718597)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2535550196:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 32.37/4.88 % (3718593)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 32.37/4.88 % Exception at run slice level
% 32.37/4.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 32.37/4.88 % (3718605)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=898960740:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi)
% 32.37/4.88 % Exception at run slice level
% 32.37/4.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 32.37/4.88 % (3718507)Instruction limit reached!
% 32.37/4.88 % (3718507)------------------------------
% 32.37/4.88 % (3718507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.37/4.88 % (3718507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.37/4.88 % (3718507)CaDiCaL version: 2.1.3
% 32.37/4.88 % (3718507)Termination reason: Instruction limit
% 32.37/4.88 % (3718507)Termination phase: Saturation
% 32.37/4.88 % (3718507)Time elapsed: 0.310 s
% 32.37/4.88 % (3718507)Peak memory usage: 14 MB
% 32.37/4.88 % (3718507)Instructions burned: 692 (million)
% 32.37/4.88 % (3718619)ott-2_1_sil=16000:newcnf=on:random_seed=3671884305:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi)
% 32.37/4.88 % (3718620)ott+10_1_sil=32000:tgt=ground:random_seed=2081339957:i=5114:av=off_2995 on theBenchmark for (2995ds/5114Mi)
% 32.37/4.88 % (3718619)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 32.37/4.88 % (3718515)Instruction limit reached!
% 32.37/4.88 % (3718515)------------------------------
% 32.37/4.88 % (3718515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.37/4.88 % (3718515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.37/4.88 % (3718515)CaDiCaL version: 2.1.3
% 32.37/4.88 % (3718515)Termination reason: Instruction limit
% 32.37/4.88 % (3718515)Termination phase: Saturation
% 32.37/4.88 % (3718515)Time elapsed: 0.412 s
% 32.37/4.88 % (3718515)Peak memory usage: 16 MB
% 32.37/4.88 % (3718515)Instructions burned: 879 (million)
% 32.37/4.88 % (3718665)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3420167713:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 32.37/4.88 % Exception at run slice level
% 98.66/14.14 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 98.66/14.14 % (3718667)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4029758842:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi)
% 98.66/14.14 % (3718667)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 98.66/14.14 % (3718619)Instruction limit reached!
% 98.66/14.14 % (3718619)------------------------------
% 98.66/14.14 % (3718619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.66/14.14 % (3718619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.66/14.14 % (3718619)CaDiCaL version: 2.1.3
% 98.66/14.14 % (3718619)Termination reason: Instruction limit
% 98.66/14.14 % (3718619)Termination phase: Saturation
% 98.66/14.14 % (3718619)Time elapsed: 0.371 s
% 98.66/14.14 % (3718619)Peak memory usage: 15 MB
% 98.66/14.14 % (3718619)Instructions burned: 870 (million)
% 98.66/14.14 % (3718669)dis+21_1_sil=32000:sas=cadical:random_seed=2021765513:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi)
% 98.66/14.14 % (3718593)Instruction limit reached!
% 98.66/14.14 % (3718593)------------------------------
% 98.66/14.14 % (3718593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.66/14.14 % (3718593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.66/14.14 % (3718593)CaDiCaL version: 2.1.3
% 98.66/14.14 % (3718593)Termination reason: Instruction limit
% 98.66/14.14 % (3718593)Termination phase: Saturation
% 98.66/14.14 % (3718593)Time elapsed: 0.657 s
% 98.66/14.14 % (3718593)Peak memory usage: 17 MB
% 98.66/14.14 % (3718593)Instructions burned: 1474 (million)
% 98.66/14.14 % (3718671)ott+11_1_sil=16000:gs=on:random_seed=2927581881:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi)
% 98.66/14.14 % (3718671)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 98.66/14.14 % (3718591)Instruction limit reached!
% 98.66/14.14 % (3718591)------------------------------
% 98.66/14.14 % (3718591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.66/14.14 % (3718591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.66/14.14 % (3718591)CaDiCaL version: 2.1.3
% 98.66/14.14 % (3718591)Termination reason: Instruction limit
% 98.66/14.14 % (3718591)Termination phase: Saturation
% 98.66/14.14 % (3718591)Time elapsed: 1.180 s
% 98.66/14.14 % (3718591)Peak memory usage: 28 MB
% 98.66/14.14 % (3718591)Instructions burned: 5135 (million)
% 98.66/14.14 % (3718673)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=449893285:fmbsr=1.6:i=67534_2984 on theBenchmark for (2984ds/67534Mi)
% 98.66/14.14 % Exception at run slice level
% 98.66/14.14 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 98.66/14.14 % (3718675)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=512311735:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2983 on theBenchmark for (2983ds/4591Mi)
% 98.66/14.14 % (3718671)Instruction limit reached!
% 98.66/14.14 % (3718671)------------------------------
% 98.66/14.14 % (3718671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.66/14.14 % (3718671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.66/14.14 % (3718671)CaDiCaL version: 2.1.3
% 98.66/14.14 % (3718671)Termination reason: Instruction limit
% 98.66/14.14 % (3718671)Termination phase: Saturation
% 98.66/14.14 % (3718671)Time elapsed: 0.987 s
% 98.66/14.14 % (3718671)Peak memory usage: 22 MB
% 98.66/14.14 % (3718671)Instructions burned: 2253 (million)
% 98.66/14.14 % (3718677)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3319134588:i=29340_2979 on theBenchmark for (2979ds/29340Mi)
% 98.66/14.14 % (3718667)Instruction limit reached!
% 98.66/14.14 % (3718667)------------------------------
% 98.66/14.14 % (3718667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.66/14.14 % (3718667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.66/14.14 % (3718667)CaDiCaL version: 2.1.3
% 98.66/14.14 % (3718667)Termination reason: Instruction limit
% 98.66/14.14 % (3718667)Termination phase: Saturation
% 98.66/14.14 % (3718667)Time elapsed: 1.535 s
% 98.66/14.14 % (3718667)Peak memory usage: 23 MB
% 98.66/14.14 % (3718667)Instructions burned: 3514 (million)
% 98.66/14.14 % (3718679)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4249920307:i=5211_2977 on theBenchmark for (2977ds/5211Mi)
% 101.15/14.55 % (3718669)Instruction limit reached!
% 101.15/14.55 % (3718669)------------------------------
% 101.15/14.55 % (3718669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.15/14.55 % (3718669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/14.55 % (3718669)CaDiCaL version: 2.1.3
% 101.15/14.55 % (3718669)Termination reason: Instruction limit
% 101.15/14.55 % (3718669)Termination phase: Saturation
% 101.15/14.55 % (3718669)Time elapsed: 1.657 s
% 101.15/14.55 % (3718669)Peak memory usage: 24 MB
% 101.15/14.55 % (3718669)Instructions burned: 3773 (million)
% 101.15/14.55 % (3718681)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3788318799:i=5497:nm=2_2974 on theBenchmark for (2974ds/5497Mi)
% 101.15/14.55 % Exception at run slice level
% 101.15/14.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.15/14.55 % (3718683)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=18875223:fmbsr=2:i=46332_2974 on theBenchmark for (2974ds/46332Mi)
% 101.15/14.55 % Exception at run slice level
% 101.15/14.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.15/14.55 % (3718685)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=846700314:i=14071_2973 on theBenchmark for (2973ds/14071Mi)
% 101.15/14.55 % Exception at run slice level
% 101.15/14.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.15/14.55 % (3718687)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3797166836:i=22565:add=on:rawr=on_2973 on theBenchmark for (2973ds/22565Mi)
% 101.15/14.55 % (3718675)Instruction limit reached!
% 101.15/14.55 % (3718675)------------------------------
% 101.15/14.55 % (3718675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.15/14.55 % (3718675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/14.55 % (3718675)CaDiCaL version: 2.1.3
% 101.15/14.55 % (3718675)Termination reason: Instruction limit
% 101.15/14.55 % (3718675)Termination phase: Saturation
% 101.15/14.55 % (3718675)Time elapsed: 1.083 s
% 101.15/14.55 % (3718675)Peak memory usage: 26 MB
% 101.15/14.55 % (3718675)Instructions burned: 4595 (million)
% 101.15/14.55 % (3718689)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=771102374:i=8173:av=off_2972 on theBenchmark for (2972ds/8173Mi)
% 101.15/14.55 % (3718620)Instruction limit reached!
% 101.15/14.55 % (3718620)------------------------------
% 101.15/14.55 % (3718620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.15/14.55 % (3718620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/14.55 % (3718620)CaDiCaL version: 2.1.3
% 101.15/14.55 % (3718620)Termination reason: Instruction limit
% 101.15/14.55 % (3718620)Termination phase: Saturation
% 101.15/14.55 % (3718620)Time elapsed: 2.216 s
% 101.15/14.55 % (3718620)Peak memory usage: 34 MB
% 101.15/14.55 % (3718620)Instructions burned: 5115 (million)
% 101.15/14.55 % (3718691)dis+10_16:1_sil=16000:random_seed=3808727008:i=9155:fsr=off_2972 on theBenchmark for (2972ds/9155Mi)
% 101.15/14.55 % (3718679)Instruction limit reached!
% 101.15/14.55 % (3718679)------------------------------
% 101.15/14.55 % (3718679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.15/14.55 % (3718679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/14.55 % (3718679)CaDiCaL version: 2.1.3
% 101.15/14.55 % (3718679)Termination reason: Instruction limit
% 101.15/14.55 % (3718679)Termination phase: Saturation
% 101.15/14.55 % (3718679)Time elapsed: 2.313 s
% 101.15/14.55 % (3718679)Peak memory usage: 33 MB
% 101.15/14.55 % (3718679)Instructions burned: 5213 (million)
% 101.15/14.55 % (3718693)ott-3_8_sil=64000:random_seed=3052674557:i=20139:bs=on_2954 on theBenchmark for (2954ds/20139Mi)
% 101.15/14.55 % (3718689)Instruction limit reached!
% 101.15/14.55 % (3718689)------------------------------
% 101.15/14.55 % (3718689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.15/14.55 % (3718689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/14.55 % (3718689)CaDiCaL version: 2.1.3
% 101.15/14.55 % (3718689)Termination reason: Instruction limit
% 101.15/14.55 % (3718689)Termination phase: Saturation
% 101.15/14.55 % (3718689)Time elapsed: 1.913 s
% 101.15/14.55 % (3718689)Peak memory usage: 44 MB
% 101.15/14.55 % (3718689)Instructions burned: 8177 (million)
% 101.15/14.55 % (3718695)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=61506301:fmbsr=2:i=32576_2953 on theBenchmark for (2953ds/32576Mi)
% 101.15/14.55 % Exception at run slice level
% 101.15/14.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.15/14.55 % (3718697)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=121541516:i=11404_2953 on theBenchmark for (2953ds/11404Mi)
% 101.15/14.55 % (3718691)Instruction limit reached!
% 101.15/14.55 % (3718691)------------------------------
% 101.15/14.55 % (3718691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.15/14.55 % (3718691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/14.55 % (3718691)CaDiCaL version: 2.1.3
% 101.15/14.55 % (3718691)Termination reason: Instruction limit
% 101.15/14.55 % (3718691)Termination phase: Saturation
% 101.15/14.55 % (3718691)Time elapsed: 3.999 s
% 101.15/14.55 % (3718691)Peak memory usage: 36 MB
% 101.15/14.55 % (3718691)Instructions burned: 9156 (million)
% 101.15/14.55 % (3718699)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3420455981:i=14134_2932 on theBenchmark for (2932ds/14134Mi)
% 101.15/14.55 % (3718699)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 101.15/14.56 % (3718697)Instruction limit reached!
% 101.15/14.56 % (3718697)------------------------------
% 101.15/14.56 % (3718697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.15/14.56 % (3718697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/14.56 % (3718697)CaDiCaL version: 2.1.3
% 101.15/14.56 % (3718697)Termination reason: Instruction limit
% 101.15/14.56 % (3718697)Termination phase: Saturation
% 101.15/14.56 % (3718697)Time elapsed: 2.713 s
% 101.15/14.56 % (3718697)Peak memory usage: 61 MB
% 101.15/14.56 % (3718697)Instructions burned: 11405 (million)
% 101.15/14.56 % (3718701)dis+33_16_sil=32000:sac=on:random_seed=3814950810:i=15851:nm=0_2926 on theBenchmark for (2926ds/15851Mi)
% 101.15/14.56 % (3718701)Instruction limit reached!
% 101.15/14.56 % (3718701)------------------------------
% 101.15/14.56 % (3718701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.15/14.56 % (3718701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/14.56 % (3718701)CaDiCaL version: 2.1.3
% 101.15/14.56 % (3718701)Termination reason: Instruction limit
% 101.15/14.56 % (3718701)Termination phase: Saturation
% 101.15/14.56 % (3718701)Time elapsed: 3.647 s
% 101.15/14.56 % (3718701)Peak memory usage: 47 MB
% 101.15/14.56 % (3718701)Instructions burned: 15856 (million)
% 101.15/14.56 % (3718703)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=155611785:avsq=on:i=17627:add=on:amm=off_2889 on theBenchmark for (2889ds/17627Mi)
% 101.15/14.56 % (3718699)Instruction limit reached!
% 101.15/14.56 % (3718699)------------------------------
% 101.15/14.56 % (3718699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.15/14.56 % (3718699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/14.56 % (3718699)CaDiCaL version: 2.1.3
% 101.15/14.56 % (3718699)Termination reason: Instruction limit
% 101.15/14.56 % (3718699)Termination phase: Saturation
% 101.15/14.56 % (3718699)Time elapsed: 6.198 s
% 101.15/14.56 % (3718699)Peak memory usage: 62 MB
% 101.15/14.56 % (3718699)Instructions burned: 14135 (million)
% 101.15/14.56 % (3718705)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=27963961:s2a=on:i=53295_2870 on theBenchmark for (2870ds/53295Mi)
% 101.15/14.56 % (3718693)Instruction limit reached!
% 101.15/14.56 % (3718693)------------------------------
% 101.15/14.56 % (3718693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.15/14.56 % (3718693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/14.56 % (3718693)CaDiCaL version: 2.1.3
% 101.15/14.56 % (3718693)Termination reason: Instruction limit
% 101.15/14.56 % (3718693)Termination phase: Saturation
% 101.15/14.56 % (3718693)Time elapsed: 8.797 s
% 101.15/14.56 % (3718693)Peak memory usage: 57 MB
% 101.15/14.56 % (3718693)Instructions burned: 20140 (million)
% 101.15/14.56 % (3718707)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=878202181:i=26857:ins=20_2866 on theBenchmark for (2866ds/26857Mi)
% 101.15/14.56 % Exception at run slice level
% 101.15/14.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.15/14.56 % (3718709)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4254912133:i=28120:bs=on:fsr=off_2866 on theBenchmark for (2866ds/28120Mi)
% 101.15/14.56 % (3718687)Instruction limit reached!
% 101.15/14.56 % (3718687)------------------------------
% 101.15/14.56 % (3718687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.15/14.56 % (3718687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/14.56 % (3718687)CaDiCaL version: 2.1.3
% 101.15/14.56 % (3718687)Termination reason: Instruction limit
% 101.15/14.56 % (3718687)Termination phase: Saturation
% 101.15/14.56 % (3718687)Time elapsed: 11.230 s
% 101.15/14.56 % (3718687)Peak memory usage: 85 MB
% 101.15/14.56 % (3718687)Instructions burned: 22565 (million)
% 101.15/14.56 % (3718868)fmb+10_1_sil=256000:fmbss=7:random_seed=274341834:fmbsr=1.6:i=182295_2860 on theBenchmark for (2860ds/182295Mi)
% 101.15/14.56 % Exception at run slice level
% 101.15/14.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.15/14.56 % (3718885)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3340458283:i=44625:gsp=on_2860 on theBenchmark for (2860ds/44625Mi)
% 101.15/14.56 % (3718885)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 101.15/14.56 % (3718885)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 101.15/14.56 % Exception at run slice level
% 101.15/14.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.15/14.56 % (3718906)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3892310372:i=160505_2860 on theBenchmark for (2860ds/160505Mi)
% 101.15/14.56 % Exception at run slice level
% 101.15/14.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.15/14.56 % (3718915)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3840365470:fmbsr=1.3:i=225729_2859 on theBenchmark for (2859ds/225729Mi)
% 101.15/14.56 % Exception at run slice level
% 101.15/14.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.15/14.56 % (3718927)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=902989751:fmbsr=2:i=185024:ins=7_2859 on theBenchmark for (2859ds/185024Mi)
% 101.15/14.56 % Exception at run slice level
% 101.15/14.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.15/14.56 % (3718941)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3693332577:rtra=on_2859 on theBenchmark for (2859ds/0Mi)
% 101.15/14.56 % Exception at run slice level
% 101.15/14.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.15/14.56 % (3718946)% WARNING: option uhcvi not known.
% 101.15/14.56 % (3718946)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1295456724:i=271062:add=off:rtra=on:rawr=on_2858 on theBenchmark for (2858ds/271062Mi)
% 101.15/14.56 % (3718946)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 101.15/14.56 % (3718946)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 101.15/14.56 % (3718705) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3718441-3718705"...
% 101.15/14.56 % (3718705)...printing done.
% 101.15/14.56 % (3718705)Refutation found. Thanks to Tanya!
% 101.15/14.56 % SZS status Theorem for theBenchmark
% 101.15/14.56 % SZS output start Proof for theBenchmark
% 101.15/14.56 thf(type_def_5, type, num: $tType).
% 101.15/14.56 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 101.15/14.56 thf(func_def_1, type, attribute_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_2, type, before_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_4, type, contraryAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_5, type, contraryAttribute_THFTYPE_IioI: ($i > $o)).
% 101.15/14.56 thf(func_def_6, type, disjointRelation_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_7, type, disjoint_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_9, type, domainSubclass_THFTYPE_IIiiiIiioI: (($i > $i > $i) > $i > $i > $o)).
% 101.15/14.56 thf(func_def_10, type, domainSubclass_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 101.15/14.56 thf(func_def_11, type, domainSubclass_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 101.15/14.56 thf(func_def_12, type, domain_THFTYPE_IIIiiiIiioIiioI: ((($i > $i > $i) > $i > $i > $o) > $i > $i > $o)).
% 101.15/14.56 thf(func_def_13, type, domain_THFTYPE_IIIiioIIiioIoIiioI: ((($i > $i > $o) > ($i > $i > $o) > $o) > $i > $i > $o)).
% 101.15/14.56 thf(func_def_14, type, domain_THFTYPE_IIiiIiioI: (($i > $i) > $i > $i > $o)).
% 101.15/14.56 thf(func_def_15, type, domain_THFTYPE_IIiiiIiioI: (($i > $i > $i) > $i > $i > $o)).
% 101.15/14.56 thf(func_def_16, type, domain_THFTYPE_IIiiioIiioI: (($i > $i > $i > $o) > $i > $i > $o)).
% 101.15/14.56 thf(func_def_17, type, domain_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 101.15/14.56 thf(func_def_18, type, domain_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 101.15/14.56 thf(func_def_19, type, duration_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_21, type, father_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_22, type, greaterThanOrEqualTo_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_23, type, greaterThan_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_24, type, gt_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_25, type, gtet_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_26, type, holdsDuring_THFTYPE_IiooI: ($i > $o > $o)).
% 101.15/14.56 thf(func_def_27, type, husband_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_28, type, inList_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_29, type, instance_THFTYPE_IIIiiiIiioIioI: ((($i > $i > $i) > $i > $i > $o) > $i > $o)).
% 101.15/14.56 thf(func_def_30, type, instance_THFTYPE_IIIiioIIiioIoIioI: ((($i > $i > $o) > ($i > $i > $o) > $o) > $i > $o)).
% 101.15/14.56 thf(func_def_31, type, instance_THFTYPE_IIIiioIiioIioI: ((($i > $i > $o) > $i > $i > $o) > $i > $o)).
% 101.15/14.56 thf(func_def_32, type, instance_THFTYPE_IIiiIioI: (($i > $i) > $i > $o)).
% 101.15/14.56 thf(func_def_33, type, instance_THFTYPE_IIiiiIioI: (($i > $i > $i) > $i > $o)).
% 101.15/14.56 thf(func_def_34, type, instance_THFTYPE_IIiiioIioI: (($i > $i > $i > $o) > $i > $o)).
% 101.15/14.56 thf(func_def_35, type, instance_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 101.15/14.56 thf(func_def_36, type, instance_THFTYPE_IIiooIioI: (($i > $o > $o) > $i > $o)).
% 101.15/14.56 thf(func_def_37, type, instance_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_39, type, inverse_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 101.15/14.56 thf(func_def_42, type, lBeginFn_THFTYPE_IiiI: ($i > $i)).
% 101.15/14.56 thf(func_def_48, type, lCardinalityFn_THFTYPE_IiiI: ($i > $i)).
% 101.15/14.56 thf(func_def_53, type, lEndFn_THFTYPE_IiiI: ($i > $i)).
% 101.15/14.56 thf(func_def_61, type, lListFn_THFTYPE_IiiI: ($i > $i)).
% 101.15/14.56 thf(func_def_64, type, lMeasureFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 101.15/14.56 thf(func_def_81, type, lTemporalCompositionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 101.15/14.56 thf(func_def_91, type, lWhenFn_THFTYPE_IiiI: ($i > $i)).
% 101.15/14.56 thf(func_def_94, type, lYearFn_THFTYPE_IiiI: ($i > $i)).
% 101.15/14.56 thf(func_def_97, type, lessThanOrEqualTo_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_98, type, lessThan_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_99, type, located_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_100, type, lt_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_101, type, ltet_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_102, type, meetsTemporally_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_103, type, minus_THFTYPE_IiiiI: ($i > $i > $i)).
% 101.15/14.56 thf(func_def_104, type, mother_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_110, type, orientation_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 101.15/14.56 thf(func_def_111, type, parent_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_112, type, part_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_113, type, partition_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 101.15/14.56 thf(func_def_115, type, rangeSubclass_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_116, type, range_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_117, type, relatedInternalConcept_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 101.15/14.56 thf(func_def_118, type, relatedInternalConcept_THFTYPE_IiIiiIoI: ($i > ($i > $i) > $o)).
% 101.15/14.56 thf(func_def_119, type, relatedInternalConcept_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_122, type, subAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_123, type, subProcess_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_124, type, subclass_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_125, type, subrelation_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 101.15/14.56 thf(func_def_126, type, subrelation_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 101.15/14.56 thf(func_def_127, type, subrelation_THFTYPE_IIioIIioIoI: (($i > $o) > ($i > $o) > $o)).
% 101.15/14.56 thf(func_def_128, type, subrelation_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_129, type, temporalPart_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_130, type, wife_THFTYPE_IiioI: ($i > $i > $o)).
% 101.15/14.56 thf(func_def_132, type, vNOT: ($o > $o)).
% 101.15/14.56 thf(func_def_135, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 101.15/14.56 thf(func_def_136, type, vAND: ($o > $o > $o)).
% 101.15/14.56 thf(func_def_137, type, sK0: (($i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_138, type, sK1: (($i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_139, type, sK2: (($i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_140, type, sK3: (($i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_141, type, sK4: (($i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_142, type, sK5: (($i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_143, type, sK6: ($i > $i)).
% 101.15/14.56 thf(func_def_144, type, sK7: ($i > $i)).
% 101.15/14.56 thf(func_def_145, type, sK8: ($i > $i)).
% 101.15/14.56 thf(func_def_147, type, sK10: ($i > $i > $i)).
% 101.15/14.56 thf(func_def_149, type, db0: !>[X0: $tType]:(X0)).
% 101.15/14.56 thf(func_def_150, type, db1: !>[X0: $tType]:(X0)).
% 101.15/14.56 thf(func_def_151, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 101.15/14.56 thf(func_def_152, type, db2: !>[X0: $tType]:(X0)).
% 101.15/14.56 thf(func_def_153, type, db3: !>[X0: $tType]:(X0)).
% 101.15/14.56 thf(func_def_154, type, db4: !>[X0: $tType]:(X0)).
% 101.15/14.56 thf(func_def_155, type, sK12: ($i > $i)).
% 101.15/14.56 thf(func_def_156, type, sK13: ($i > ($i > $i > $i > $i) > $i)).
% 101.15/14.56 thf(func_def_157, type, sK14: ($i > ($i > $i > $i > $i) > $i)).
% 101.15/14.56 thf(func_def_158, type, sK15: ($i > ($i > $i > $i > $i) > $i)).
% 101.15/14.56 thf(func_def_159, type, sK16: ($i > ($i > $i > $i > $i) > $i)).
% 101.15/14.56 thf(func_def_160, type, sK17: ($i > ($i > $i > $i > $i) > $i)).
% 101.15/14.56 thf(func_def_161, type, sK18: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_162, type, sK19: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_163, type, sK20: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_164, type, sK21: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_165, type, sK22: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_166, type, sK23: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_167, type, sK24: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_168, type, sK25: ($i > ($i > $i > $i > $o > $o) > $i)).
% 101.15/14.56 thf(func_def_169, type, sK26: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_170, type, sK27: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_171, type, sK28: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_172, type, sK29: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_173, type, sK30: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_174, type, sK31: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_175, type, sK32: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_176, type, sK33: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_177, type, sK34: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_178, type, sK35: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_179, type, sK36: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_180, type, sK37: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_181, type, sK38: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_182, type, sK39: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_183, type, sK40: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_184, type, sK41: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_185, type, sK42: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_186, type, sK43: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_187, type, sK44: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_188, type, sK45: ($i > ($i > $i > $i > $i > $o) > $i)).
% 101.15/14.56 thf(func_def_189, type, sK46: ($i > ($i > $i > $i > $i > $i) > $i)).
% 101.15/14.56 thf(func_def_190, type, sK47: ($i > ($i > $i > $i > $i > $i) > $i)).
% 101.15/14.56 thf(f6,axiom,(
% 101.15/14.56 ! [X0 : ($i > $i > $o),X1 : ($i > $i > $o)] : ((inverse_THFTYPE_IIiioIIiioIoI @ X1 @ X0) => ! [X2 : $i,X3 : $i] : ((X1 @ X2 @ X3) <=> (X0 @ X3 @ X2)))),
% 101.15/14.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_005)).
% 101.15/14.56 thf(f48,axiom,(
% 101.15/14.56 ! [X0 : $i] : (holdsDuring_THFTYPE_IiooI @ X0 @ $true)),
% 101.15/14.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_047)).
% 101.15/14.56 thf(f76,axiom,(
% 101.15/14.56 ! [X0 : $i,X1 : $o] : ((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1)) => (~ (holdsDuring_THFTYPE_IiooI @ X0 @ X1)))),
% 101.15/14.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_075)).
% 101.15/14.56 thf(f83,axiom,(
% 101.15/14.56 (inverse_THFTYPE_IIiioIIiioIoI @ husband_THFTYPE_IiioI @ wife_THFTYPE_IiioI)),
% 101.15/14.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_082)).
% 101.15/14.56 thf(f95,axiom,(
% 101.15/14.56 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ lChris_THFTYPE_i))),
% 101.15/14.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_094)).
% 101.15/14.56 thf(f298,conjecture,(
% 101.15/14.56 ? [X0 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (husband_THFTYPE_IiioI @ X0 @ lCorina_THFTYPE_i))),
% 101.15/14.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 101.15/14.56 thf(f299,negated_conjecture,(
% 101.15/14.56 ~ ? [X0 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (husband_THFTYPE_IiioI @ X0 @ lCorina_THFTYPE_i))),
% 101.15/14.56 inference(negated_conjecture,[status(cth)],[f298])).
% 101.15/14.56 thf(f310,plain,(
% 101.15/14.56 ! [X0 : ($i > $i > $o),X1 : ($i > $i > $o)] : ((inverse_THFTYPE_IIiioIIiioIoI @ X1 @ X0) => ! [X2 : $i,X3 : $i] : ((X1 @ X2 @ X3) <=> (X0 @ X3 @ X2)))),
% 101.15/14.56 inference(rectify,[],[f6])).
% 101.15/14.56 thf(f311,plain,(
% 101.15/14.56 ! [X0 : ($i > $i > $o),X1 : ($i > $i > $o)] : ((((inverse_THFTYPE_IIiioIIiioIoI @ X1 @ X0)) = $true) => ! [X2 : $i,X3 : $i] : (((X1 @ X2 @ X3)) = ((X0 @ X3 @ X2))))),
% 101.15/14.56 inference(fool_elimination,[],[f310])).
% 101.15/14.56 thf(f392,plain,(
% 101.15/14.56 ! [X0 : $i] : (holdsDuring_THFTYPE_IiooI @ X0 @ $true)),
% 101.15/14.56 inference(rectify,[],[f48])).
% 101.15/14.56 thf(f393,plain,(
% 101.15/14.56 ! [X0 : $i] : ($true = ((holdsDuring_THFTYPE_IiooI @ X0 @ $true)))),
% 101.15/14.56 inference(fool_elimination,[],[f392])).
% 101.15/14.56 thf(f448,plain,(
% 101.15/14.56 ! [X0 : $i,X1 : $o] : ((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1)) => (~ (holdsDuring_THFTYPE_IiooI @ X0 @ X1)))),
% 101.15/14.56 inference(rectify,[],[f76])).
% 101.15/14.56 thf(f449,plain,(
% 101.15/14.56 ! [X0 : $i,X1 : $o] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1))) = $true) => (((~ (holdsDuring_THFTYPE_IiooI @ X0 @ X1))) = $true))),
% 101.15/14.56 inference(fool_elimination,[],[f448])).
% 101.15/14.56 thf(f462,plain,(
% 101.15/14.56 (inverse_THFTYPE_IIiioIIiioIoI @ husband_THFTYPE_IiioI @ wife_THFTYPE_IiioI)),
% 101.15/14.56 inference(rectify,[],[f83])).
% 101.15/14.56 thf(f463,plain,(
% 101.15/14.56 (((inverse_THFTYPE_IIiioIIiioIoI @ husband_THFTYPE_IiioI @ wife_THFTYPE_IiioI)) = $true)),
% 101.15/14.56 inference(fool_elimination,[],[f462])).
% 101.15/14.56 thf(f486,plain,(
% 101.15/14.56 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ lChris_THFTYPE_i))),
% 101.15/14.56 inference(rectify,[],[f95])).
% 101.15/14.56 thf(f487,plain,(
% 101.15/14.56 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ lChris_THFTYPE_i))) = $true)),
% 101.15/14.56 inference(fool_elimination,[],[f486])).
% 101.15/14.56 thf(f892,plain,(
% 101.15/14.56 ~ ? [X0 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (husband_THFTYPE_IiioI @ X0 @ lCorina_THFTYPE_i))),
% 101.15/14.56 inference(rectify,[],[f299])).
% 101.15/14.56 thf(f893,plain,(
% 101.15/14.56 ~ ? [X0 : $i] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (husband_THFTYPE_IiioI @ X0 @ lCorina_THFTYPE_i))) = $true)),
% 101.15/14.56 inference(fool_elimination,[],[f892])).
% 101.15/14.56 thf(f902,plain,(
% 101.15/14.56 ! [X0 : ($i > $i > $o),X1 : ($i > $i > $o)] : (! [X2 : $i,X3 : $i] : (((X1 @ X2 @ X3)) = ((X0 @ X3 @ X2))) | (((inverse_THFTYPE_IIiioIIiioIoI @ X1 @ X0)) != $true))),
% 101.15/14.56 inference(ennf_transformation,[],[f311])).
% 101.15/14.56 thf(f955,plain,(
% 101.15/14.56 ! [X0 : $i,X1 : $o] : ((((~ (holdsDuring_THFTYPE_IiooI @ X0 @ X1))) = $true) | (((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1))) != $true))),
% 101.15/14.56 inference(ennf_transformation,[],[f449])).
% 101.15/14.56 thf(f975,plain,(
% 101.15/14.56 ! [X0 : $i] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (husband_THFTYPE_IiioI @ X0 @ lCorina_THFTYPE_i))) != $true)),
% 101.15/14.56 inference(ennf_transformation,[],[f893])).
% 101.15/14.56 thf(f1003,plain,(
% 101.15/14.56 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i > $o),X1 : ($i > $i > $o)] : ((((X1 @ X2 @ X3)) = ((X0 @ X3 @ X2))) | (((inverse_THFTYPE_IIiioIIiioIoI @ X1 @ X0)) != $true)) )),
% 101.15/14.56 inference(cnf_transformation,[],[f902])).
% 101.15/14.56 thf(f1051,plain,(
% 101.15/14.56 ( ! [X0 : $i] : (($true = ((holdsDuring_THFTYPE_IiooI @ X0 @ $true)))) )),
% 101.15/14.56 inference(cnf_transformation,[],[f393])).
% 101.15/14.56 thf(f1085,plain,(
% 101.15/14.56 ( ! [X0 : $i,X1 : $o] : ((((~ (holdsDuring_THFTYPE_IiooI @ X0 @ X1))) = $true) | (((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1))) != $true)) )),
% 101.15/14.56 inference(cnf_transformation,[],[f955])).
% 101.15/14.56 thf(f1093,plain,(
% 101.15/14.56 (((inverse_THFTYPE_IIiioIIiioIoI @ husband_THFTYPE_IiioI @ wife_THFTYPE_IiioI)) = $true)),
% 101.15/14.56 inference(cnf_transformation,[],[f463])).
% 101.15/14.56 thf(f1106,plain,(
% 101.15/14.56 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ lChris_THFTYPE_i))) = $true)),
% 101.15/14.56 inference(cnf_transformation,[],[f487])).
% 101.15/14.56 thf(f1309,plain,(
% 101.15/14.56 ( ! [X0 : $i] : ((((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (husband_THFTYPE_IiioI @ X0 @ lCorina_THFTYPE_i))) != $true)) )),
% 101.15/14.56 inference(cnf_transformation,[],[f975])).
% 101.15/14.56 thf(f1311,definition,(
% 101.15/14.56 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 101.15/14.56 introduced(theory,[fool_exhaustiveness_axiom])).
% 101.15/14.56 thf(f1325,plain,(
% 101.15/14.56 ( ! [X0 : $i,X1 : $o] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false) | (((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1))) != $true)) )),
% 101.15/14.56 inference(not_proxy_clausification,[],[f1085])).
% 101.15/14.56 thf(f1337,plain,(
% 101.15/14.56 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i > $o),X1 : ($i > $i > $o)] : ((((X1 @ X2 @ X3)) = $true) | (((inverse_THFTYPE_IIiioIIiioIoI @ X1 @ X0)) != $true) | (((X0 @ X3 @ X2)) = $false)) )),
% 101.15/14.56 inference(iff_proxy_clausification,[],[f1003])).
% 101.15/14.56 thf(f1340,definition,(
% 101.15/14.56 spl11_1 <=> ! [X0 : $i] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (husband_THFTYPE_IiioI @ X0 @ lCorina_THFTYPE_i))) != $true)),
% 101.15/14.56 introduced(definition,[new_symbols(definition,[spl11_1])],[avatar_definition])).
% 101.15/14.56 thf(f1341,plain,(
% 101.15/14.56 ( ! [X0 : $i] : ((((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (husband_THFTYPE_IiioI @ X0 @ lCorina_THFTYPE_i))) != $true)) ) | ~spl11_1),
% 101.15/14.56 inference(avatar_component_clause,[],[f1340])).
% 101.15/14.56 thf(f1342,plain,(
% 101.15/14.56 spl11_1),
% 101.15/14.56 inference(avatar_split_clause,[],[f1309,f1340])).
% 101.15/14.56 thf(f2387,definition,(
% 101.15/14.56 spl11_216 <=> (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ lChris_THFTYPE_i))) = $true)),
% 101.15/14.56 introduced(definition,[new_symbols(definition,[spl11_216])],[avatar_definition])).
% 101.15/14.56 thf(f2389,plain,(
% 101.15/14.56 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ lChris_THFTYPE_i))) = $true) | ~spl11_216),
% 101.15/14.56 inference(avatar_component_clause,[],[f2387])).
% 101.15/14.56 thf(f2390,plain,(
% 101.15/14.56 spl11_216),
% 101.15/14.56 inference(avatar_split_clause,[],[f1106,f2387])).
% 101.15/14.56 thf(f2503,definition,(
% 101.15/14.56 spl11_249 <=> (((inverse_THFTYPE_IIiioIIiioIoI @ husband_THFTYPE_IiioI @ wife_THFTYPE_IiioI)) = $true)),
% 101.15/14.56 introduced(definition,[new_symbols(definition,[spl11_249])],[avatar_definition])).
% 101.15/14.56 thf(f2505,plain,(
% 101.15/14.56 (((inverse_THFTYPE_IIiioIIiioIoI @ husband_THFTYPE_IiioI @ wife_THFTYPE_IiioI)) = $true) | ~spl11_249),
% 101.15/14.56 inference(avatar_component_clause,[],[f2503])).
% 101.15/14.56 thf(f2506,plain,(
% 101.15/14.56 spl11_249),
% 101.15/14.56 inference(avatar_split_clause,[],[f1093,f2503])).
% 101.15/14.56 thf(f2567,definition,(
% 101.15/14.56 spl11_266 <=> ! [X0 : $i,X1 : $o] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false) | (((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1))) != $true))),
% 101.15/14.56 introduced(definition,[new_symbols(definition,[spl11_266])],[avatar_definition])).
% 101.15/14.56 thf(f2568,plain,(
% 101.15/14.56 ( ! [X0 : $i,X1 : $o] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1))) != $true) | (((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false)) ) | ~spl11_266),
% 101.15/14.56 inference(avatar_component_clause,[],[f2567])).
% 101.15/14.56 thf(f2569,plain,(
% 101.15/14.56 spl11_266),
% 101.15/14.56 inference(avatar_split_clause,[],[f1325,f2567])).
% 101.15/14.56 thf(f2803,definition,(
% 101.15/14.56 spl11_330 <=> ! [X0 : $i] : ($true = ((holdsDuring_THFTYPE_IiooI @ X0 @ $true)))),
% 101.15/14.56 introduced(definition,[new_symbols(definition,[spl11_330])],[avatar_definition])).
% 101.15/14.56 thf(f2804,plain,(
% 101.15/14.56 ( ! [X0 : $i] : (($true = ((holdsDuring_THFTYPE_IiooI @ X0 @ $true)))) ) | ~spl11_330),
% 101.15/14.56 inference(avatar_component_clause,[],[f2803])).
% 101.15/14.56 thf(f2805,plain,(
% 101.15/14.56 spl11_330),
% 101.15/14.56 inference(avatar_split_clause,[],[f1051,f2803])).
% 101.15/14.56 thf(f3122,definition,(
% 101.15/14.56 spl11_414 <=> ! [X0 : ($i > $i > $o),X3 : $i,X2 : $i,X1 : ($i > $i > $o)] : ((((X1 @ X2 @ X3)) = $true) | (((inverse_THFTYPE_IIiioIIiioIoI @ X1 @ X0)) != $true) | (((X0 @ X3 @ X2)) = $false))),
% 101.15/14.56 introduced(definition,[new_symbols(definition,[spl11_414])],[avatar_definition])).
% 101.15/14.56 thf(f3123,plain,(
% 101.15/14.56 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i > $o),X1 : ($i > $i > $o)] : ((((inverse_THFTYPE_IIiioIIiioIoI @ X1 @ X0)) != $true) | (((X1 @ X2 @ X3)) = $true) | (((X0 @ X3 @ X2)) = $false)) ) | ~spl11_414),
% 101.15/14.56 inference(avatar_component_clause,[],[f3122])).
% 101.15/14.56 thf(f3124,plain,(
% 101.15/14.56 spl11_414),
% 101.15/14.56 inference(avatar_split_clause,[],[f1337,f3122])).
% 101.15/14.56 thf(f3173,definition,(
% 101.15/14.56 spl11_428 <=> ! [X0 : $o] : (($true = X0) | ($false = X0))),
% 101.15/14.56 introduced(definition,[new_symbols(definition,[spl11_428])],[avatar_definition])).
% 101.15/14.56 thf(f3174,plain,(
% 101.15/14.56 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) ) | ~spl11_428),
% 101.15/14.56 inference(avatar_component_clause,[],[f3173])).
% 101.15/14.56 thf(f3175,plain,(
% 101.15/14.56 spl11_428),
% 101.15/14.56 inference(avatar_split_clause,[],[f1311,f3173])).
% 101.15/14.56 thf(f12066,plain,(
% 101.15/14.56 ( ! [X0 : $i,X1 : $o] : (($true != ((holdsDuring_THFTYPE_IiooI @ X0 @ $true))) | (((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false) | (((~ X1)) = $false)) ) | (~spl11_266 | ~spl11_428)),
% 101.15/14.56 inference(constrained_superposition,[],[f2568,f3174])).
% 101.15/14.56 thf(f12072,plain,(
% 101.15/14.56 ( ! [X0 : $i,X1 : $o] : (($true != ((holdsDuring_THFTYPE_IiooI @ X0 @ $true))) | (((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false) | ($true = X1)) ) | (~spl11_266 | ~spl11_428)),
% 101.15/14.56 inference(not_proxy_clausification,[],[f12066])).
% 101.15/14.56 thf(f12074,definition,(
% 101.15/14.56 spl11_1445 <=> ! [X0 : $i,X1 : $o] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false) | ($true = X1))),
% 101.15/14.56 introduced(definition,[new_symbols(definition,[spl11_1445])],[avatar_definition])).
% 101.15/14.56 thf(f12075,plain,(
% 101.15/14.56 ( ! [X0 : $i,X1 : $o] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false) | ($true = X1)) ) | ~spl11_1445),
% 101.15/14.56 inference(avatar_component_clause,[],[f12074])).
% 101.15/14.56 thf(f12081,plain,(
% 101.15/14.56 ( ! [X0 : $i,X1 : $o] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false) | ($true = X1)) ) | (~spl11_266 | ~spl11_330 | ~spl11_428)),
% 101.15/14.56 inference(forward_subsumption_resolution,[],[f12072,f2804])).
% 101.15/14.56 thf(f12082,plain,(
% 101.15/14.56 spl11_1445 | ~spl11_266 | ~spl11_330 | ~spl11_428),
% 101.15/14.56 inference(avatar_split_clause,[],[f12081,f3173,f2803,f2567,f12074])).
% 101.15/14.56 thf(f12089,plain,(
% 101.15/14.56 ($true = $false) | (((wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ lChris_THFTYPE_i)) = $true) | (~spl11_216 | ~spl11_1445)),
% 101.15/14.56 inference(constrained_superposition,[],[f2389,f12075])).
% 101.15/14.56 thf(f12093,plain,(
% 101.15/14.56 (((wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ lChris_THFTYPE_i)) = $true) | (~spl11_216 | ~spl11_1445)),
% 101.15/14.56 inference(trivial_inequality_removal,[],[f12089])).
% 101.15/14.56 thf(f12201,definition,(
% 101.15/14.56 spl11_1460 <=> (((wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ lChris_THFTYPE_i)) = $true)),
% 101.15/14.56 introduced(definition,[new_symbols(definition,[spl11_1460])],[avatar_definition])).
% 101.15/14.56 thf(f12203,plain,(
% 101.15/14.56 (((wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ lChris_THFTYPE_i)) = $true) | ~spl11_1460),
% 101.15/14.56 inference(avatar_component_clause,[],[f12201])).
% 101.15/14.56 thf(f12204,plain,(
% 101.15/14.56 spl11_1460 | ~spl11_216 | ~spl11_1445),
% 101.15/14.56 inference(avatar_split_clause,[],[f12093,f12074,f2387,f12201])).
% 101.15/14.56 thf(f23398,plain,(
% 101.15/14.56 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true = ((husband_THFTYPE_IiioI @ X0 @ X1))) | ($false = ((wife_THFTYPE_IiioI @ X1 @ X0)))) ) | (~spl11_249 | ~spl11_414)),
% 101.15/14.56 inference(constrained_superposition,[],[f3123,f2505])).
% 101.15/14.56 thf(f23399,plain,(
% 101.15/14.56 ( ! [X0 : $i,X1 : $i] : (($true = ((husband_THFTYPE_IiioI @ X0 @ X1))) | ($false = ((wife_THFTYPE_IiioI @ X1 @ X0)))) ) | (~spl11_249 | ~spl11_414)),
% 101.15/14.56 inference(trivial_inequality_removal,[],[f23398])).
% 101.15/14.56 thf(f23622,definition,(
% 101.15/14.56 spl11_2767 <=> ! [X0 : $i,X1 : $i] : (($true = ((husband_THFTYPE_IiioI @ X0 @ X1))) | ($false = ((wife_THFTYPE_IiioI @ X1 @ X0))))),
% 101.15/14.56 introduced(definition,[new_symbols(definition,[spl11_2767])],[avatar_definition])).
% 101.15/14.56 thf(f23623,plain,(
% 101.15/14.56 ( ! [X0 : $i,X1 : $i] : (($true = ((husband_THFTYPE_IiioI @ X0 @ X1))) | ($false = ((wife_THFTYPE_IiioI @ X1 @ X0)))) ) | ~spl11_2767),
% 101.15/14.56 inference(avatar_component_clause,[],[f23622])).
% 101.15/14.56 thf(f23624,plain,(
% 101.15/14.56 spl11_2767 | ~spl11_249 | ~spl11_414),
% 101.15/14.56 inference(avatar_split_clause,[],[f23399,f3122,f2503,f23622])).
% 101.15/14.56 thf(f27098,plain,(
% 101.15/14.56 ( ! [X0 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ($false = ((wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ X0)))) ) | (~spl11_1 | ~spl11_2767)),
% 101.15/14.56 inference(constrained_superposition,[],[f1341,f23623])).
% 101.15/14.56 thf(f27111,plain,(
% 101.15/14.56 ( ! [X0 : $i] : (($false = ((wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ X0)))) ) | (~spl11_1 | ~spl11_330 | ~spl11_2767)),
% 101.15/14.56 inference(forward_subsumption_resolution,[],[f27098,f2804])).
% 101.15/14.56 thf(f27113,definition,(
% 101.15/14.56 spl11_2977 <=> ! [X0 : $i] : ($false = ((wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ X0)))),
% 101.15/14.56 introduced(definition,[new_symbols(definition,[spl11_2977])],[avatar_definition])).
% 101.15/14.56 thf(f27114,plain,(
% 101.15/14.56 ( ! [X0 : $i] : (($false = ((wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ X0)))) ) | ~spl11_2977),
% 101.15/14.56 inference(avatar_component_clause,[],[f27113])).
% 101.15/14.56 thf(f27125,plain,(
% 101.15/14.56 spl11_2977 | ~spl11_1 | ~spl11_330 | ~spl11_2767),
% 101.15/14.56 inference(avatar_split_clause,[],[f27111,f23622,f2803,f1340,f27113])).
% 101.15/14.56 thf(f27128,plain,(
% 101.15/14.56 ($true = $false) | (~spl11_1460 | ~spl11_2977)),
% 101.15/14.56 inference(constrained_superposition,[],[f27114,f12203])).
% 101.15/14.56 thf(f27133,plain,(
% 101.15/14.56 $false | (~spl11_1460 | ~spl11_2977)),
% 101.15/14.56 inference(trivial_inequality_removal,[],[f27128])).
% 101.15/14.56 thf(f27134,plain,(
% 101.15/14.56 ~spl11_1460 | ~spl11_2977),
% 101.15/14.56 inference(avatar_contradiction_clause,[],[f27133])).
% 101.15/14.56 cnf(s1, plain, spl11_1, inference(sat_conversion,[],[f1342])).
% 101.15/14.56 cnf(s204, plain, spl11_216, inference(sat_conversion,[],[f2390])).
% 101.15/14.56 cnf(s218, plain, spl11_249, inference(sat_conversion,[],[f2506])).
% 101.15/14.56 cnf(s226, plain, spl11_266, inference(sat_conversion,[],[f2569])).
% 101.15/14.56 cnf(s260, plain, spl11_330, inference(sat_conversion,[],[f2805])).
% 101.15/14.56 cnf(s311, plain, spl11_414, inference(sat_conversion,[],[f3124])).
% 101.15/14.56 cnf(s319, plain, spl11_428, inference(sat_conversion,[],[f3175])).
% 101.15/14.56 cnf(s2248, plain, ~spl11_266 | ~spl11_330 | ~spl11_428 | spl11_1445, inference(sat_conversion,[],[f12082])).
% 101.15/14.56 cnf(s2264, plain, ~spl11_216 | ~spl11_1445 | spl11_1460, inference(sat_conversion,[],[f12204])).
% 101.15/14.56 cnf(s4855, plain, ~spl11_249 | ~spl11_414 | spl11_2767, inference(sat_conversion,[],[f23624])).
% 101.15/14.56 cnf(s5517, plain, ~spl11_1 | ~spl11_330 | ~spl11_2767 | spl11_2977, inference(sat_conversion,[],[f27125])).
% 101.15/14.56 cnf(s5520, plain, ~spl11_1460 | ~spl11_2977, inference(sat_conversion,[],[f27134])).
% 101.15/14.56 cnf(s5705, plain, spl11_1445, inference(rat,[],[s2248,s260,s319,s226])).
% 101.15/14.56 cnf(s5721, plain, spl11_2767, inference(rat,[],[s4855,s311,s218])).
% 101.15/14.56 cnf(s5751, plain, spl11_1460, inference(rat,[],[s2264,s5705,s204])).
% 101.15/14.56 cnf(s5753, plain, ~spl11_2977, inference(rat,[],[s5520,s5751])).
% 101.15/14.56 cnf(s5760, plain, ~spl11_1, inference(rat,[],[s5517,s5721,s260,s5753])).
% 101.15/14.56 cnf(s6412, plain, $false, inference(rat,[],[s1,s5760])).
% 101.15/14.56 thf(f27138,plain,(
% 101.15/14.56 $false),
% 101.15/14.56 inference(avatar_sat_refutation,[],[s6412])).
% 101.15/14.56 % SZS output end Proof for theBenchmark
% 101.15/14.56 % (3718705)------------------------------
% 101.15/14.56 % (3718705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.15/14.56 % (3718705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/14.56 % (3718705)CaDiCaL version: 2.1.3
% 101.15/14.56 % (3718705)Termination reason: Refutation
% 101.15/14.56 % (3718705)Time elapsed: 1.308 s
% 101.15/14.56 % (3718705)Peak memory usage: 29 MB
% 101.15/14.56 % (3718705)Instructions burned: 2928 (million)
% 101.15/14.56 % (3718441)Success in time 14.324 s
% 101.15/14.56 % Vampire exiting
%------------------------------------------------------------------------------