Vampire-SAT---5.0.1.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire-SAT---5.0.1
% Problem  : GEG002^1 : TPTP v9.3.1. Released v4.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT

% Computer : n018.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:49:27 AM UTC 2026

% Result   : Theorem 4.04s 1.02s
% Output   : Refutation 4.04s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GEG002^1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19  % Computer : n018.cluster.edu
% 0.08/0.19  % Model    : x86_64 x86_64
% 0.08/0.19  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19  % Memory   : 8046.5625MB
% 0.08/0.19  % OS       : Linux 6.8.0-71-generic
% 0.08/0.19  % CPULimit : 300
% 0.08/0.19  % WCLimit  : 300
% 0.08/0.19  % DateTime : Tue Sep 29 18:35:57 UTC 2026
% 0.08/0.19  % CPUTime  : 
% 0.08/0.19  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22  Running first-order model finding
% 0.08/0.22  Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.04/1.02  % (469175)Will run a generic schedule for satisfiability detection.
% 4.04/1.02  % (469186)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3502293606:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.04/1.02  % (469181)% WARNING: option uhcvi not known.
% 4.04/1.02  % (469182)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3873071435:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.04/1.02  % (469180)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1428288729_2999 on theBenchmark for (2999ds/0Mi)
% 4.04/1.02  % (469181)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2305854855:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.04/1.02  % (469183)dis+10_1_sil=32000:sp=arity:random_seed=291360485:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.04/1.02  % (469181)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.04/1.02  % Exception at run slice level
% 4.04/1.02  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.04/1.02  % (469181)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.04/1.02  % (469184)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2131535289:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.04/1.02  % (469184)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.04/1.02  % (469185)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3051690530:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.04/1.02  % (469193)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3295616120:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.04/1.02  % Exception at run slice level
% 4.04/1.02  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.04/1.02  % (469186)Instruction limit reached! 
% 4.04/1.02  % (469186)------------------------------
% 4.04/1.02  % (469186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/1.02  % (469186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/1.02  % (469186)CaDiCaL version: 2.1.3
% 4.04/1.02  % (469186)Termination reason: Instruction limit
% 4.04/1.02  % (469186)Termination phase: Saturation
% 4.04/1.02  % (469186)Time elapsed: 0.046 s
% 4.04/1.02  % (469186)Peak memory usage: 13 MB
% 4.04/1.02  % (469186)Instructions burned: 160 (million)
% 4.04/1.02  % (469196)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2342577298:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.04/1.02  % (469183)Instruction limit reached! 
% 4.04/1.02  % (469183)------------------------------
% 4.04/1.02  % (469183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/1.02  % (469183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/1.02  % (469183)CaDiCaL version: 2.1.3
% 4.04/1.02  % (469183)Termination reason: Instruction limit
% 4.04/1.02  % (469183)Termination phase: Saturation
% 4.04/1.02  % (469183)Time elapsed: 0.050 s
% 4.04/1.02  % (469183)Peak memory usage: 12 MB
% 4.04/1.02  % (469183)Instructions burned: 104 (million)
% 4.04/1.02  % (469197)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=889376851:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.04/1.02  % (469197)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.04/1.02  % (469197)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.04/1.02  % (469199)ott-21_1_sil=16000:fs=off:random_seed=448946151:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.04/1.02  % (469184)Instruction limit reached! 
% 4.04/1.02  % (469184)------------------------------
% 4.04/1.02  % (469184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/1.02  % (469184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/1.02  % (469184)CaDiCaL version: 2.1.3
% 4.04/1.02  % (469184)Termination reason: Instruction limit
% 4.04/1.02  % (469184)Termination phase: Saturation
% 4.04/1.02  % (469184)Time elapsed: 0.074 s
% 4.04/1.02  % (469184)Peak memory usage: 12 MB
% 4.04/1.02  % (469184)Instructions burned: 116 (million)
% 4.04/1.02  % (469202)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=139441504:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 4.04/1.02  % (469196)Instruction limit reached! 
% 4.04/1.02  % (469196)------------------------------
% 4.04/1.02  % (469196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/1.02  % (469196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/1.02  % (469196)CaDiCaL version: 2.1.3
% 4.04/1.02  % (469196)Termination reason: Instruction limit
% 4.04/1.02  % (469196)Termination phase: Saturation
% 4.04/1.02  % (469196)Time elapsed: 0.064 s
% 4.04/1.02  % (469196)Peak memory usage: 12 MB
% 4.04/1.02  % (469196)Instructions burned: 133 (million)
% 4.04/1.02  % (469185)Instruction limit reached! 
% 4.04/1.02  % (469185)------------------------------
% 4.04/1.02  % (469185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/1.02  % (469185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/1.02  % (469185)CaDiCaL version: 2.1.3
% 4.04/1.02  % (469185)Termination reason: Instruction limit
% 4.04/1.02  % (469185)Termination phase: Saturation
% 4.04/1.02  % (469185)Time elapsed: 0.113 s
% 4.04/1.02  % (469185)Peak memory usage: 12 MB
% 4.04/1.02  % (469185)Instructions burned: 131 (million)
% 4.04/1.02  % (469204)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2626946907:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 4.04/1.02  % Exception at run slice level
% 4.04/1.02  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.04/1.02  % (469205)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2197366165:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 4.04/1.02  % (469207)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4202209766:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 4.04/1.02  % Exception at run slice level
% 4.04/1.02  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.04/1.02  % (469199)Instruction limit reached! 
% 4.04/1.02  % (469199)------------------------------
% 4.04/1.02  % (469199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/1.02  % (469199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/1.02  % (469199)CaDiCaL version: 2.1.3
% 4.04/1.02  % (469199)Termination reason: Instruction limit
% 4.04/1.02  % (469199)Termination phase: Saturation
% 4.04/1.02  % (469199)Time elapsed: 0.099 s
% 4.04/1.02  % (469199)Peak memory usage: 13 MB
% 4.04/1.02  % (469199)Instructions burned: 180 (million)
% 4.04/1.02  % (469210)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=1450288239: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)
% 4.04/1.02  % (469210)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.04/1.02  % (469211)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1931559759:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 4.04/1.02  % (469211)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.04/1.02  % (469197)Instruction limit reached! 
% 4.04/1.02  % (469197)------------------------------
% 4.04/1.02  % (469197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/1.02  % (469197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/1.02  % (469197)CaDiCaL version: 2.1.3
% 4.04/1.02  % (469197)Termination reason: Instruction limit
% 4.04/1.02  % (469197)Termination phase: Saturation
% 4.04/1.02  % (469197)Time elapsed: 0.165 s
% 4.04/1.02  % (469197)Peak memory usage: 14 MB
% 4.04/1.02  % (469197)Instructions burned: 686 (million)
% 4.04/1.02  % (469214)fmb+10_1_sil=64000:random_seed=666889674:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 4.04/1.02  % (469214)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 4.04/1.02  % Exception at run slice level
% 4.04/1.02  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.04/1.02  % (469216)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3737567547:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 4.04/1.02  % Exception at run slice level
% 4.04/1.02  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.04/1.02  % (469218)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3568079149:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 4.04/1.02  % Exception at run slice level
% 4.04/1.02  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.04/1.02  % (469220)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3857771139:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 4.04/1.02  % (469220)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.04/1.02  % (469202)Instruction limit reached! 
% 4.04/1.02  % (469202)------------------------------
% 4.04/1.02  % (469202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/1.02  % (469202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/1.02  % (469202)CaDiCaL version: 2.1.3
% 4.04/1.02  % (469202)Termination reason: Instruction limit
% 4.04/1.02  % (469202)Termination phase: Saturation
% 4.04/1.02  % (469202)Time elapsed: 0.261 s
% 4.04/1.02  % (469202)Peak memory usage: 13 MB
% 4.04/1.02  % (469202)Instructions burned: 478 (million)
% 4.04/1.02  % (469222)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2827540772:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi)
% 4.04/1.02  % (469222)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 4.04/1.02  % (469222)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.04/1.02  % (469210)Instruction limit reached! 
% 4.04/1.02  % (469210)------------------------------
% 4.04/1.02  % (469210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/1.02  % (469210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/1.02  % (469210)CaDiCaL version: 2.1.3
% 4.04/1.02  % (469210)Termination reason: Instruction limit
% 4.04/1.02  % (469210)Termination phase: Saturation
% 4.04/1.02  % (469210)Time elapsed: 0.332 s
% 4.04/1.02  % (469210)Peak memory usage: 15 MB
% 4.04/1.02  % (469210)Instructions burned: 693 (million)
% 4.04/1.02  % (469224)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3495389604:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 4.04/1.02  % Exception at run slice level
% 4.04/1.02  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.04/1.02  % (469226)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3916057532:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 4.04/1.02  % Exception at run slice level
% 4.04/1.02  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.04/1.02  % (469228)ott-2_1_sil=16000:newcnf=on:random_seed=1592772377:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 4.04/1.02  % (469228)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.04/1.02  % (469211)Instruction limit reached! 
% 4.04/1.02  % (469211)------------------------------
% 4.04/1.02  % (469211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/1.02  % (469211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/1.02  % (469211)CaDiCaL version: 2.1.3
% 4.04/1.02  % (469211)Termination reason: Instruction limit
% 4.04/1.02  % (469211)Termination phase: Saturation
% 4.04/1.02  % (469211)Time elapsed: 0.521 s
% 4.04/1.02  % (469211)Peak memory usage: 14 MB
% 4.04/1.02  % (469211)Instructions burned: 880 (million)
% 4.04/1.02  % (469230)ott+10_1_sil=32000:tgt=ground:random_seed=4290683464:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 4.04/1.02  % (469228) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-469175-469228"...
% 4.04/1.02  % (469228)...printing done.
% 4.04/1.02  % (469228)Refutation found. Thanks to Tanya!
% 4.04/1.02  % SZS status Theorem for theBenchmark
% 4.04/1.02  % SZS output start Proof for theBenchmark
% 4.04/1.02  thf(type_def_5, type, reg: $tType).
% 4.04/1.02  thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 4.04/1.02  thf(func_def_0, type, c: (reg > reg > $o)).
% 4.04/1.02  thf(func_def_1, type, dc: (reg > reg > $o)).
% 4.04/1.02  thf(func_def_2, type, p: (reg > reg > $o)).
% 4.04/1.02  thf(func_def_3, type, eq: (reg > reg > $o)).
% 4.04/1.02  thf(func_def_4, type, o: (reg > reg > $o)).
% 4.04/1.02  thf(func_def_5, type, po: (reg > reg > $o)).
% 4.04/1.02  thf(func_def_6, type, ec: (reg > reg > $o)).
% 4.04/1.02  thf(func_def_7, type, pp: (reg > reg > $o)).
% 4.04/1.02  thf(func_def_8, type, tpp: (reg > reg > $o)).
% 4.04/1.02  thf(func_def_9, type, ntpp: (reg > reg > $o)).
% 4.04/1.02  thf(func_def_11, type, catalunya: reg).
% 4.04/1.02  thf(func_def_12, type, france: reg).
% 4.04/1.02  thf(func_def_13, type, spain: reg).
% 4.04/1.02  thf(func_def_14, type, paris: reg).
% 4.04/1.02  thf(func_def_17, type, vNOT: ($o > $o)).
% 4.04/1.02  thf(func_def_18, type, db1: !>[X0: $tType]:(X0)).
% 4.04/1.02  thf(func_def_19, type, db0: !>[X0: $tType]:(X0)).
% 4.04/1.02  thf(func_def_20, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 4.04/1.02  thf(func_def_21, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 4.04/1.02  thf(func_def_22, type, vIMP: ($o > $o > $o)).
% 4.04/1.02  thf(func_def_23, type, db2: !>[X0: $tType]:(X0)).
% 4.04/1.02  thf(func_def_24, type, vAND: ($o > $o > $o)).
% 4.04/1.02  thf(func_def_25, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 4.04/1.02  thf(func_def_26, type, sK0: reg).
% 4.04/1.02  thf(func_def_27, type, sK1: (reg > reg)).
% 4.04/1.02  thf(func_def_28, type, sK2: (reg > reg)).
% 4.04/1.02  thf(func_def_29, type, sK3: (reg > reg)).
% 4.04/1.02  thf(func_def_30, type, sK4: (reg > reg)).
% 4.04/1.02  thf(func_def_31, type, sK5: reg).
% 4.04/1.02  thf(func_def_32, type, sK6: reg).
% 4.04/1.02  thf(func_def_33, type, sK7: (reg > reg)).
% 4.04/1.02  thf(func_def_34, type, sK8: (reg > reg)).
% 4.04/1.02  thf(func_def_35, type, sK9: (reg > reg)).
% 4.04/1.02  thf(func_def_36, type, sK10: (reg > reg)).
% 4.04/1.02  thf(f2,axiom,(
% 4.04/1.02    ! [X0 : reg,X1 : reg] : ((c @ X0 @ X1) => (c @ X1 @ X0))),
% 4.04/1.02    file('/export/starexec/sandbox2/benchmark/Axioms/LCL014^0.ax',c_symmetric)).
% 4.04/1.02  thf(f3,axiom,(
% 4.04/1.02    (dc = (^[X0 : reg, X1 : reg] : (~(c @ X0 @ X1))))),
% 4.04/1.02    file('/export/starexec/sandbox2/benchmark/Axioms/LCL014^0.ax',dc)).
% 4.04/1.02  thf(f4,axiom,(
% 4.04/1.02    (p = (^[X0 : reg, X1 : reg] : (! [X2 : reg] : ((c @ X2 @ X0) => (c @ X2 @ X1)))))),
% 4.04/1.02    file('/export/starexec/sandbox2/benchmark/Axioms/LCL014^0.ax',p)).
% 4.04/1.02  thf(f6,axiom,(
% 4.04/1.02    (o = (^[X0 : reg, X1 : reg] : (? [X2 : reg] : ((p @ X2 @ X1) & (p @ X2 @ X0)))))),
% 4.04/1.02    file('/export/starexec/sandbox2/benchmark/Axioms/LCL014^0.ax',o)).
% 4.04/1.02  thf(f8,axiom,(
% 4.04/1.02    (ec = (^[X0 : reg, X1 : reg] : (~(o @ X0 @ X1) & (c @ X0 @ X1))))),
% 4.04/1.02    file('/export/starexec/sandbox2/benchmark/Axioms/LCL014^0.ax',ec)).
% 4.04/1.02  thf(f9,axiom,(
% 4.04/1.02    (pp = (^[X0 : reg, X1 : reg] : (~(p @ X1 @ X0) & (p @ X0 @ X1))))),
% 4.04/1.02    file('/export/starexec/sandbox2/benchmark/Axioms/LCL014^0.ax',pp)).
% 4.04/1.02  thf(f10,axiom,(
% 4.04/1.02    (tpp = (^[X0 : reg, X1 : reg] : (? [X2 : reg] : ((ec @ X2 @ X1) & (ec @ X2 @ X0)) & (pp @ X0 @ X1))))),
% 4.04/1.02    file('/export/starexec/sandbox2/benchmark/Axioms/LCL014^0.ax',tpp)).
% 4.04/1.02  thf(f11,axiom,(
% 4.04/1.02    (ntpp = (^[X0 : reg, X1 : reg] : (~ ? [X2 : reg] : ((ec @ X2 @ X1) & (ec @ X2 @ X0)) & (pp @ X0 @ X1))))),
% 4.04/1.02    file('/export/starexec/sandbox2/benchmark/Axioms/LCL014^0.ax',ntpp)).
% 4.04/1.02  thf(f12,axiom,(
% 4.04/1.02    (tpp @ catalunya @ spain)),
% 4.04/1.02    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1)).
% 4.04/1.02  thf(f13,axiom,(
% 4.04/1.02    (ec @ spain @ france)),
% 4.04/1.02    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2)).
% 4.04/1.02  thf(f14,axiom,(
% 4.04/1.02    (ntpp @ paris @ france)),
% 4.04/1.02    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3)).
% 4.04/1.02  thf(f15,conjecture,(
% 4.04/1.02    (dc @ spain @ paris) & (dc @ catalunya @ paris)),
% 4.04/1.02    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',con)).
% 4.04/1.02  thf(f16,negated_conjecture,(
% 4.04/1.02    ~((dc @ spain @ paris) & (dc @ catalunya @ paris))),
% 4.04/1.02    inference(negated_conjecture,[status(cth)],[f15])).
% 4.04/1.02  thf(f19,plain,(
% 4.04/1.02    ! [X0 : reg,X1 : reg] : ((c @ X0 @ X1) => (c @ X1 @ X0))),
% 4.04/1.02    inference(rectify,[],[f2])).
% 4.04/1.02  thf(f20,plain,(
% 4.04/1.02    ! [X0 : reg,X1 : reg] : ((((c @ X0 @ X1)) = $true) => (((c @ X1 @ X0)) = $true))),
% 4.04/1.02    inference(fool_elimination,[],[f19])).
% 4.04/1.02  thf(f21,plain,(
% 4.04/1.02    (dc = (^[X0 : reg, X1 : reg] : (~(c @ X0 @ X1))))),
% 4.04/1.02    inference(rectify,[],[f3])).
% 4.04/1.02  thf(f22,plain,(
% 4.04/1.02    (dc = (^[Y0 : reg]: ((^[Y1 : reg]: (~ (c @ Y0 @ Y1))))))),
% 4.04/1.02    inference(fool_elimination,[],[f21])).
% 4.04/1.02  thf(f23,plain,(
% 4.04/1.02    (p = (^[X0 : reg, X1 : reg] : (! [X2 : reg] : ((c @ X2 @ X0) => (c @ X2 @ X1)))))),
% 4.04/1.02    inference(rectify,[],[f4])).
% 4.04/1.02  thf(f24,plain,(
% 4.04/1.02    (p = (^[Y0 : reg]: ((^[Y1 : reg]: (!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y0) => (c @ Y2 @ Y1))))))))),
% 4.04/1.02    inference(fool_elimination,[],[f23])).
% 4.04/1.02  thf(f27,plain,(
% 4.04/1.02    (o = (^[X0 : reg, X1 : reg] : (? [X2 : reg] : ((p @ X2 @ X1) & (p @ X2 @ X0)))))),
% 4.04/1.02    inference(rectify,[],[f6])).
% 4.04/1.02  thf(f28,plain,(
% 4.04/1.02    (o = (^[Y0 : reg]: ((^[Y1 : reg]: (?? @ reg @ (^[Y2 : reg]: ((p @ Y2 @ Y0) & (p @ Y2 @ Y1))))))))),
% 4.04/1.02    inference(fool_elimination,[],[f27])).
% 4.04/1.02  thf(f31,plain,(
% 4.04/1.02    (ec = (^[X0 : reg, X1 : reg] : (~(o @ X0 @ X1) & (c @ X0 @ X1))))),
% 4.04/1.02    inference(rectify,[],[f8])).
% 4.04/1.02  thf(f32,plain,(
% 4.04/1.02    (ec = (^[Y0 : reg]: ((^[Y1 : reg]: ((c @ Y0 @ Y1) & (~ (o @ Y0 @ Y1)))))))),
% 4.04/1.02    inference(fool_elimination,[],[f31])).
% 4.04/1.02  thf(f33,plain,(
% 4.04/1.02    (pp = (^[X0 : reg, X1 : reg] : (~(p @ X1 @ X0) & (p @ X0 @ X1))))),
% 4.04/1.02    inference(rectify,[],[f9])).
% 4.04/1.02  thf(f34,plain,(
% 4.04/1.02    (pp = (^[Y0 : reg]: ((^[Y1 : reg]: ((p @ Y0 @ Y1) & (~ (p @ Y1 @ Y0)))))))),
% 4.04/1.02    inference(fool_elimination,[],[f33])).
% 4.04/1.02  thf(f35,plain,(
% 4.04/1.02    (tpp = (^[X0 : reg, X1 : reg] : (? [X2 : reg] : ((ec @ X2 @ X1) & (ec @ X2 @ X0)) & (pp @ X0 @ X1))))),
% 4.04/1.02    inference(rectify,[],[f10])).
% 4.04/1.02  thf(f36,plain,(
% 4.04/1.02    (tpp = (^[Y0 : reg]: ((^[Y1 : reg]: ((pp @ Y0 @ Y1) & (?? @ reg @ (^[Y2 : reg]: ((ec @ Y2 @ Y0) & (ec @ Y2 @ Y1)))))))))),
% 4.04/1.02    inference(fool_elimination,[],[f35])).
% 4.04/1.02  thf(f37,plain,(
% 4.04/1.02    (ntpp = (^[X0 : reg, X1 : reg] : (~ ? [X2 : reg] : ((ec @ X2 @ X1) & (ec @ X2 @ X0)) & (pp @ X0 @ X1))))),
% 4.04/1.02    inference(rectify,[],[f11])).
% 4.04/1.02  thf(f38,plain,(
% 4.04/1.02    (ntpp = (^[Y0 : reg]: ((^[Y1 : reg]: ((pp @ Y0 @ Y1) & (~ (?? @ reg @ (^[Y2 : reg]: ((ec @ Y2 @ Y0) & (ec @ Y2 @ Y1))))))))))),
% 4.04/1.02    inference(fool_elimination,[],[f37])).
% 4.04/1.02  thf(f39,plain,(
% 4.04/1.02    (tpp @ catalunya @ spain)),
% 4.04/1.02    inference(rectify,[],[f12])).
% 4.04/1.02  thf(f40,plain,(
% 4.04/1.02    (((tpp @ catalunya @ spain)) = $true)),
% 4.04/1.02    inference(fool_elimination,[],[f39])).
% 4.04/1.02  thf(f41,plain,(
% 4.04/1.02    (ec @ spain @ france)),
% 4.04/1.02    inference(rectify,[],[f13])).
% 4.04/1.02  thf(f42,plain,(
% 4.04/1.02    (((ec @ spain @ france)) = $true)),
% 4.04/1.02    inference(fool_elimination,[],[f41])).
% 4.04/1.02  thf(f43,plain,(
% 4.04/1.02    (ntpp @ paris @ france)),
% 4.04/1.02    inference(rectify,[],[f14])).
% 4.04/1.02  thf(f44,plain,(
% 4.04/1.02    (((ntpp @ paris @ france)) = $true)),
% 4.04/1.02    inference(fool_elimination,[],[f43])).
% 4.04/1.02  thf(f45,plain,(
% 4.04/1.02    ~((dc @ spain @ paris) & (dc @ catalunya @ paris))),
% 4.04/1.02    inference(rectify,[],[f16])).
% 4.04/1.02  thf(f46,plain,(
% 4.04/1.02    ~((((dc @ spain @ paris)) = $true) & (((dc @ catalunya @ paris)) = $true))),
% 4.04/1.02    inference(fool_elimination,[],[f45])).
% 4.04/1.02  thf(f47,plain,(
% 4.04/1.02    ! [X0 : reg,X1 : reg] : ((((c @ X1 @ X0)) = $true) | (((c @ X0 @ X1)) != $true))),
% 4.04/1.02    inference(ennf_transformation,[],[f20])).
% 4.04/1.02  thf(f48,plain,(
% 4.04/1.02    (((dc @ spain @ paris)) != $true) | (((dc @ catalunya @ paris)) != $true)),
% 4.04/1.02    inference(ennf_transformation,[],[f46])).
% 4.04/1.02  thf(f50,plain,(
% 4.04/1.02    ( ! [X0 : reg,X1 : reg] : ((((c @ X0 @ X1)) != $true) | (((c @ X1 @ X0)) = $true)) )),
% 4.04/1.02    inference(cnf_transformation,[],[f47])).
% 4.04/1.02  thf(f51,plain,(
% 4.04/1.02    (dc = (^[Y0 : reg]: ((^[Y1 : reg]: (~ (c @ Y0 @ Y1))))))),
% 4.04/1.02    inference(cnf_transformation,[],[f22])).
% 4.04/1.02  thf(f52,plain,(
% 4.04/1.02    (p = (^[Y0 : reg]: ((^[Y1 : reg]: (!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y0) => (c @ Y2 @ Y1))))))))),
% 4.04/1.02    inference(cnf_transformation,[],[f24])).
% 4.04/1.02  thf(f54,plain,(
% 4.04/1.02    (o = (^[Y0 : reg]: ((^[Y1 : reg]: (?? @ reg @ (^[Y2 : reg]: ((p @ Y2 @ Y0) & (p @ Y2 @ Y1))))))))),
% 4.04/1.02    inference(cnf_transformation,[],[f28])).
% 4.04/1.02  thf(f56,plain,(
% 4.04/1.02    (ec = (^[Y0 : reg]: ((^[Y1 : reg]: ((c @ Y0 @ Y1) & (~ (o @ Y0 @ Y1)))))))),
% 4.04/1.02    inference(cnf_transformation,[],[f32])).
% 4.04/1.02  thf(f57,plain,(
% 4.04/1.02    (pp = (^[Y0 : reg]: ((^[Y1 : reg]: ((p @ Y0 @ Y1) & (~ (p @ Y1 @ Y0)))))))),
% 4.04/1.02    inference(cnf_transformation,[],[f34])).
% 4.04/1.02  thf(f58,plain,(
% 4.04/1.02    (tpp = (^[Y0 : reg]: ((^[Y1 : reg]: ((pp @ Y0 @ Y1) & (?? @ reg @ (^[Y2 : reg]: ((ec @ Y2 @ Y0) & (ec @ Y2 @ Y1)))))))))),
% 4.04/1.02    inference(cnf_transformation,[],[f36])).
% 4.04/1.02  thf(f59,plain,(
% 4.04/1.02    (ntpp = (^[Y0 : reg]: ((^[Y1 : reg]: ((pp @ Y0 @ Y1) & (~ (?? @ reg @ (^[Y2 : reg]: ((ec @ Y2 @ Y0) & (ec @ Y2 @ Y1))))))))))),
% 4.04/1.02    inference(cnf_transformation,[],[f38])).
% 4.04/1.02  thf(f60,plain,(
% 4.04/1.02    (((tpp @ catalunya @ spain)) = $true)),
% 4.04/1.02    inference(cnf_transformation,[],[f40])).
% 4.04/1.02  thf(f61,plain,(
% 4.04/1.02    (((ec @ spain @ france)) = $true)),
% 4.04/1.02    inference(cnf_transformation,[],[f42])).
% 4.04/1.02  thf(f62,plain,(
% 4.04/1.02    (((ntpp @ paris @ france)) = $true)),
% 4.04/1.02    inference(cnf_transformation,[],[f44])).
% 4.04/1.02  thf(f63,plain,(
% 4.04/1.02    (((dc @ spain @ paris)) != $true) | (((dc @ catalunya @ paris)) != $true)),
% 4.04/1.02    inference(cnf_transformation,[],[f48])).
% 4.04/1.02  thf(f65,definition,(
% 4.04/1.02    ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 4.04/1.02    introduced(theory,[fool_exhaustiveness_axiom])).
% 4.04/1.02  thf(f67,plain,(
% 4.04/1.02    (o = (^[Y0 : reg]: ((^[Y1 : reg]: (?? @ reg @ (^[Y2 : reg]: (((^[Y3 : reg]: ((^[Y4 : reg]: (!! @ reg @ (^[Y5 : reg]: ((c @ Y5 @ Y3) => (c @ Y5 @ Y4))))))) @ Y2 @ Y0) & ((^[Y3 : reg]: ((^[Y4 : reg]: (!! @ reg @ (^[Y5 : reg]: ((c @ Y5 @ Y3) => (c @ Y5 @ Y4))))))) @ Y2 @ Y1))))))))),
% 4.04/1.02    inference(definition_unfolding,[],[f54,f52,f52])).
% 4.04/1.02  thf(f69,plain,(
% 4.04/1.02    (ec = (^[Y0 : reg]: ((^[Y1 : reg]: ((c @ Y0 @ Y1) & (~ ((^[Y2 : reg]: ((^[Y3 : reg]: (?? @ reg @ (^[Y4 : reg]: (((^[Y5 : reg]: ((^[Y6 : reg]: (!! @ reg @ (^[Y7 : reg]: ((c @ Y7 @ Y5) => (c @ Y7 @ Y6))))))) @ Y4 @ Y2) & ((^[Y5 : reg]: ((^[Y6 : reg]: (!! @ reg @ (^[Y7 : reg]: ((c @ Y7 @ Y5) => (c @ Y7 @ Y6))))))) @ Y4 @ Y3))))))) @ Y0 @ Y1)))))))),
% 4.04/1.02    inference(definition_unfolding,[],[f56,f67])).
% 4.04/1.02  thf(f70,plain,(
% 4.04/1.02    (pp = (^[Y0 : reg]: ((^[Y1 : reg]: (((^[Y2 : reg]: ((^[Y3 : reg]: (!! @ reg @ (^[Y4 : reg]: ((c @ Y4 @ Y2) => (c @ Y4 @ Y3))))))) @ Y0 @ Y1) & (~ ((^[Y2 : reg]: ((^[Y3 : reg]: (!! @ reg @ (^[Y4 : reg]: ((c @ Y4 @ Y2) => (c @ Y4 @ Y3))))))) @ Y1 @ Y0)))))))),
% 4.04/1.02    inference(definition_unfolding,[],[f57,f52,f52])).
% 4.04/1.02  thf(f71,plain,(
% 4.04/1.02    (tpp = (^[Y0 : reg]: ((^[Y1 : reg]: (((^[Y2 : reg]: ((^[Y3 : reg]: (((^[Y4 : reg]: ((^[Y5 : reg]: (!! @ reg @ (^[Y6 : reg]: ((c @ Y6 @ Y4) => (c @ Y6 @ Y5))))))) @ Y2 @ Y3) & (~ ((^[Y4 : reg]: ((^[Y5 : reg]: (!! @ reg @ (^[Y6 : reg]: ((c @ Y6 @ Y4) => (c @ Y6 @ Y5))))))) @ Y3 @ Y2)))))) @ Y0 @ Y1) & (?? @ reg @ (^[Y2 : reg]: (((^[Y3 : reg]: ((^[Y4 : reg]: ((c @ Y3 @ Y4) & (~ ((^[Y5 : reg]: ((^[Y6 : reg]: (?? @ reg @ (^[Y7 : reg]: (((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y5) & ((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y6))))))) @ Y3 @ Y4)))))) @ Y2 @ Y0) & ((^[Y3 : reg]: ((^[Y4 : reg]: ((c @ Y3 @ Y4) & (~ ((^[Y5 : reg]: ((^[Y6 : reg]: (?? @ reg @ (^[Y7 : reg]: (((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y5) & ((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y6))))))) @ Y3 @ Y4)))))) @ Y2 @ Y1)))))))))),
% 4.04/1.02    inference(definition_unfolding,[],[f58,f70,f69,f69])).
% 4.04/1.02  thf(f72,plain,(
% 4.04/1.02    (ntpp = (^[Y0 : reg]: ((^[Y1 : reg]: (((^[Y2 : reg]: ((^[Y3 : reg]: (((^[Y4 : reg]: ((^[Y5 : reg]: (!! @ reg @ (^[Y6 : reg]: ((c @ Y6 @ Y4) => (c @ Y6 @ Y5))))))) @ Y2 @ Y3) & (~ ((^[Y4 : reg]: ((^[Y5 : reg]: (!! @ reg @ (^[Y6 : reg]: ((c @ Y6 @ Y4) => (c @ Y6 @ Y5))))))) @ Y3 @ Y2)))))) @ Y0 @ Y1) & (~ (?? @ reg @ (^[Y2 : reg]: (((^[Y3 : reg]: ((^[Y4 : reg]: ((c @ Y3 @ Y4) & (~ ((^[Y5 : reg]: ((^[Y6 : reg]: (?? @ reg @ (^[Y7 : reg]: (((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y5) & ((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y6))))))) @ Y3 @ Y4)))))) @ Y2 @ Y0) & ((^[Y3 : reg]: ((^[Y4 : reg]: ((c @ Y3 @ Y4) & (~ ((^[Y5 : reg]: ((^[Y6 : reg]: (?? @ reg @ (^[Y7 : reg]: (((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y5) & ((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y6))))))) @ Y3 @ Y4)))))) @ Y2 @ Y1))))))))))),
% 4.04/1.02    inference(definition_unfolding,[],[f59,f70,f69,f69])).
% 4.04/1.02  thf(f73,plain,(
% 4.04/1.02    ($true = (((^[Y0 : reg]: ((^[Y1 : reg]: (((^[Y2 : reg]: ((^[Y3 : reg]: (((^[Y4 : reg]: ((^[Y5 : reg]: (!! @ reg @ (^[Y6 : reg]: ((c @ Y6 @ Y4) => (c @ Y6 @ Y5))))))) @ Y2 @ Y3) & (~ ((^[Y4 : reg]: ((^[Y5 : reg]: (!! @ reg @ (^[Y6 : reg]: ((c @ Y6 @ Y4) => (c @ Y6 @ Y5))))))) @ Y3 @ Y2)))))) @ Y0 @ Y1) & (?? @ reg @ (^[Y2 : reg]: (((^[Y3 : reg]: ((^[Y4 : reg]: ((c @ Y3 @ Y4) & (~ ((^[Y5 : reg]: ((^[Y6 : reg]: (?? @ reg @ (^[Y7 : reg]: (((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y5) & ((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y6))))))) @ Y3 @ Y4)))))) @ Y2 @ Y0) & ((^[Y3 : reg]: ((^[Y4 : reg]: ((c @ Y3 @ Y4) & (~ ((^[Y5 : reg]: ((^[Y6 : reg]: (?? @ reg @ (^[Y7 : reg]: (((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y5) & ((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y6))))))) @ Y3 @ Y4)))))) @ Y2 @ Y1)))))))) @ catalunya @ spain)))),
% 4.04/1.02    inference(definition_unfolding,[],[f60,f71])).
% 4.04/1.02  thf(f74,plain,(
% 4.04/1.02    ($true = (((^[Y0 : reg]: ((^[Y1 : reg]: ((c @ Y0 @ Y1) & (~ ((^[Y2 : reg]: ((^[Y3 : reg]: (?? @ reg @ (^[Y4 : reg]: (((^[Y5 : reg]: ((^[Y6 : reg]: (!! @ reg @ (^[Y7 : reg]: ((c @ Y7 @ Y5) => (c @ Y7 @ Y6))))))) @ Y4 @ Y2) & ((^[Y5 : reg]: ((^[Y6 : reg]: (!! @ reg @ (^[Y7 : reg]: ((c @ Y7 @ Y5) => (c @ Y7 @ Y6))))))) @ Y4 @ Y3))))))) @ Y0 @ Y1)))))) @ spain @ france)))),
% 4.04/1.02    inference(definition_unfolding,[],[f61,f69])).
% 4.04/1.02  thf(f75,plain,(
% 4.04/1.02    ($true = (((^[Y0 : reg]: ((^[Y1 : reg]: (((^[Y2 : reg]: ((^[Y3 : reg]: (((^[Y4 : reg]: ((^[Y5 : reg]: (!! @ reg @ (^[Y6 : reg]: ((c @ Y6 @ Y4) => (c @ Y6 @ Y5))))))) @ Y2 @ Y3) & (~ ((^[Y4 : reg]: ((^[Y5 : reg]: (!! @ reg @ (^[Y6 : reg]: ((c @ Y6 @ Y4) => (c @ Y6 @ Y5))))))) @ Y3 @ Y2)))))) @ Y0 @ Y1) & (~ (?? @ reg @ (^[Y2 : reg]: (((^[Y3 : reg]: ((^[Y4 : reg]: ((c @ Y3 @ Y4) & (~ ((^[Y5 : reg]: ((^[Y6 : reg]: (?? @ reg @ (^[Y7 : reg]: (((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y5) & ((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y6))))))) @ Y3 @ Y4)))))) @ Y2 @ Y0) & ((^[Y3 : reg]: ((^[Y4 : reg]: ((c @ Y3 @ Y4) & (~ ((^[Y5 : reg]: ((^[Y6 : reg]: (?? @ reg @ (^[Y7 : reg]: (((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y5) & ((^[Y8 : reg]: ((^[Y9 : reg]: (!! @ reg @ (^[Y10 : reg]: ((c @ Y10 @ Y8) => (c @ Y10 @ Y9))))))) @ Y7 @ Y6))))))) @ Y3 @ Y4)))))) @ Y2 @ Y1))))))))) @ paris @ france)))),
% 4.04/1.02    inference(definition_unfolding,[],[f62,f72])).
% 4.04/1.02  thf(f76,plain,(
% 4.04/1.02    ($true != (((^[Y0 : reg]: ((^[Y1 : reg]: (~ (c @ Y0 @ Y1))))) @ spain @ paris))) | ($true != (((^[Y0 : reg]: ((^[Y1 : reg]: (~ (c @ Y0 @ Y1))))) @ catalunya @ paris)))),
% 4.04/1.02    inference(definition_unfolding,[],[f63,f51,f51])).
% 4.04/1.02  thf(f77,plain,(
% 4.04/1.02    ($true != ((~ (c @ spain @ paris)))) | ($true != ((~ (c @ catalunya @ paris))))),
% 4.04/1.02    inference(beta-eta_normalization,[],[f76])).
% 4.04/1.02  thf(f78,plain,(
% 4.04/1.02    ($true = ((c @ spain @ paris))) | ($true != ((~ (c @ catalunya @ paris))))),
% 4.04/1.02    inference(not_proxy_clausification,[],[f77])).
% 4.04/1.02  thf(f79,plain,(
% 4.04/1.02    ($true = ((c @ spain @ paris))) | ($true = ((c @ catalunya @ paris)))),
% 4.04/1.02    inference(not_proxy_clausification,[],[f78])).
% 4.04/1.02  thf(f80,plain,(
% 4.04/1.02    ($true = ((((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ paris) => (c @ Y0 @ france)))) & (~ (!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ france) => (c @ Y0 @ paris)))))) & (~ (?? @ reg @ (^[Y0 : reg]: (((c @ Y0 @ paris) & (~ (?? @ reg @ (^[Y1 : reg]: ((!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ Y0)))) & (!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ paris))))))))) & ((c @ Y0 @ france) & (~ (?? @ reg @ (^[Y1 : reg]: ((!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ Y0)))) & (!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ france))))))))))))))))),
% 4.04/1.02    inference(beta-eta_normalization,[],[f75])).
% 4.04/1.02  thf(f81,plain,(
% 4.04/1.02    ($true = ((~ (?? @ reg @ (^[Y0 : reg]: (((c @ Y0 @ paris) & (~ (?? @ reg @ (^[Y1 : reg]: ((!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ Y0)))) & (!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ paris))))))))) & ((c @ Y0 @ france) & (~ (?? @ reg @ (^[Y1 : reg]: ((!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ Y0)))) & (!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ france)))))))))))))))),
% 4.04/1.02    inference(and_proxy_clausification,[],[f80])).
% 4.04/1.02  thf(f82,plain,(
% 4.04/1.02    ($true = (((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ paris) => (c @ Y0 @ france)))) & (~ (!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ france) => (c @ Y0 @ paris))))))))),
% 4.04/1.02    inference(and_proxy_clausification,[],[f80])).
% 4.04/1.02  thf(f84,plain,(
% 4.04/1.02    ($true = ((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ paris) => (c @ Y0 @ france))))))),
% 4.04/1.02    inference(and_proxy_clausification,[],[f82])).
% 4.04/1.02  thf(f85,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = (((^[Y0 : reg]: ((c @ Y0 @ paris) => (c @ Y0 @ france))) @ X1)))) )),
% 4.04/1.02    inference(pi_proxy_clausification,[],[f84])).
% 4.04/1.02  thf(f86,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = (((c @ X1 @ paris) => (c @ X1 @ france))))) )),
% 4.04/1.02    inference(beta-eta_normalization,[],[f85])).
% 4.04/1.02  thf(f87,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f86])).
% 4.04/1.02  thf(f93,plain,(
% 4.04/1.02    ($false = ((?? @ reg @ (^[Y0 : reg]: (((c @ Y0 @ paris) & (~ (?? @ reg @ (^[Y1 : reg]: ((!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ Y0)))) & (!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ paris))))))))) & ((c @ Y0 @ france) & (~ (?? @ reg @ (^[Y1 : reg]: ((!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ Y0)))) & (!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ france))))))))))))))),
% 4.04/1.02    inference(not_proxy_clausification,[],[f81])).
% 4.04/1.02  thf(f94,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = (((^[Y0 : reg]: (((c @ Y0 @ paris) & (~ (?? @ reg @ (^[Y1 : reg]: ((!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ Y0)))) & (!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ paris))))))))) & ((c @ Y0 @ france) & (~ (?? @ reg @ (^[Y1 : reg]: ((!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ Y0)))) & (!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ france))))))))))) @ X1)))) )),
% 4.04/1.02    inference(pi_proxy_clausification,[],[f93])).
% 4.04/1.02  thf(f95,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = ((((c @ X1 @ paris) & (~ (?? @ reg @ (^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ paris))))))))) & ((c @ X1 @ france) & (~ (?? @ reg @ (^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ france))))))))))))) )),
% 4.04/1.02    inference(beta-eta_normalization,[],[f94])).
% 4.04/1.02  thf(f96,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = (((c @ X1 @ france) & (~ (?? @ reg @ (^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ france))))))))))) | ($false = (((c @ X1 @ paris) & (~ (?? @ reg @ (^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ paris)))))))))))) )),
% 4.04/1.02    inference(and_proxy_clausification,[],[f95])).
% 4.04/1.02  thf(f97,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = ((~ (?? @ reg @ (^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ france)))))))))) | ($false = (((c @ X1 @ paris) & (~ (?? @ reg @ (^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ paris))))))))))) | ($false = ((c @ X1 @ france)))) )),
% 4.04/1.02    inference(and_proxy_clausification,[],[f96])).
% 4.04/1.02  thf(f98,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = ((?? @ reg @ (^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ france))))))))) | ($false = (((c @ X1 @ paris) & (~ (?? @ reg @ (^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ paris))))))))))) | ($false = ((c @ X1 @ france)))) )),
% 4.04/1.02    inference(not_proxy_clausification,[],[f97])).
% 4.04/1.02  thf(f99,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = (((^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ france)))))) @ (sK1 @ X1)))) | ($false = (((c @ X1 @ paris) & (~ (?? @ reg @ (^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ paris))))))))))) | ($false = ((c @ X1 @ france)))) )),
% 4.04/1.02    inference(sigma_proxy_clausification,[],[f98])).
% 4.04/1.02  thf(f100,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = (((^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ france)))))) @ (sK1 @ X1)))) | ($false = ((~ (?? @ reg @ (^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ paris)))))))))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(and_proxy_clausification,[],[f99])).
% 4.04/1.02  thf(f101,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = (((^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ france)))))) @ (sK1 @ X1)))) | ($true = ((?? @ reg @ (^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ paris))))))))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(not_proxy_clausification,[],[f100])).
% 4.04/1.02  thf(f102,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = (((^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ france)))))) @ (sK1 @ X1)))) | ($true = (((^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ X1)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ paris)))))) @ (sK2 @ X1)))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(sigma_proxy_clausification,[],[f101])).
% 4.04/1.02  thf(f103,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = (((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK1 @ X1)) => (c @ Y0 @ X1)))) & (!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK1 @ X1)) => (c @ Y0 @ france))))))) | ($true = (((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ X1)))) & (!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ paris))))))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(beta-eta_normalization,[],[f102])).
% 4.04/1.02  thf(f104,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = ((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK1 @ X1)) => (c @ Y0 @ france)))))) | ($true = (((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ X1)))) & (!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ paris))))))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(and_proxy_clausification,[],[f103])).
% 4.04/1.02  thf(f105,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = ((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK1 @ X1)) => (c @ Y0 @ X1)))))) | ($true = (((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ X1)))) & (!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ paris))))))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(and_proxy_clausification,[],[f103])).
% 4.04/1.02  thf(f106,plain,(
% 4.04/1.02    ( ! [X2 : reg,X1 : reg] : (($true = (((^[Y0 : reg]: ((c @ Y0 @ (sK1 @ X1)) => (c @ Y0 @ X1))) @ X2))) | ($true = (((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ X1)))) & (!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ paris))))))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(pi_proxy_clausification,[],[f105])).
% 4.04/1.02  thf(f107,plain,(
% 4.04/1.02    ( ! [X2 : reg,X1 : reg] : (($true = (((^[Y0 : reg]: ((c @ Y0 @ (sK1 @ X1)) => (c @ Y0 @ X1))) @ X2))) | ($true = ((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ paris)))))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(and_proxy_clausification,[],[f106])).
% 4.04/1.02  thf(f108,plain,(
% 4.04/1.02    ( ! [X2 : reg,X1 : reg] : (($true = (((^[Y0 : reg]: ((c @ Y0 @ (sK1 @ X1)) => (c @ Y0 @ X1))) @ X2))) | ($true = ((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ X1)))))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(and_proxy_clausification,[],[f106])).
% 4.04/1.02  thf(f109,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($true = (((^[Y0 : reg]: ((c @ Y0 @ (sK1 @ X1)) => (c @ Y0 @ X1))) @ X2))) | ($true = (((^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ X1))) @ X3))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(pi_proxy_clausification,[],[f108])).
% 4.04/1.02  thf(f110,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($true = (((c @ X2 @ (sK1 @ X1)) => (c @ X2 @ X1)))) | ($true = (((c @ X3 @ (sK2 @ X1)) => (c @ X3 @ X1)))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(beta-eta_normalization,[],[f109])).
% 4.04/1.02  thf(f111,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($false = ((c @ X2 @ (sK1 @ X1)))) | ($true = (((c @ X3 @ (sK2 @ X1)) => (c @ X3 @ X1)))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris))) | (((c @ X2 @ X1)) = $true)) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f110])).
% 4.04/1.02  thf(f112,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($false = ((c @ X3 @ (sK2 @ X1)))) | ($false = ((c @ X2 @ (sK1 @ X1)))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris))) | (((c @ X2 @ X1)) = $true) | ($true = ((c @ X3 @ X1)))) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f111])).
% 4.04/1.02  thf(f113,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($true = (((^[Y0 : reg]: ((c @ Y0 @ (sK1 @ X1)) => (c @ Y0 @ X1))) @ X2))) | ($true = (((^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ paris))) @ X3))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(pi_proxy_clausification,[],[f107])).
% 4.04/1.02  thf(f114,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($true = (((c @ X2 @ (sK1 @ X1)) => (c @ X2 @ X1)))) | ($true = (((c @ X3 @ (sK2 @ X1)) => (c @ X3 @ paris)))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(beta-eta_normalization,[],[f113])).
% 4.04/1.02  thf(f115,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($false = ((c @ X2 @ (sK1 @ X1)))) | ($true = (((c @ X3 @ (sK2 @ X1)) => (c @ X3 @ paris)))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris))) | (((c @ X2 @ X1)) = $true)) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f114])).
% 4.04/1.02  thf(f116,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($false = ((c @ X3 @ (sK2 @ X1)))) | ($false = ((c @ X2 @ (sK1 @ X1)))) | ($true = ((c @ X3 @ paris))) | ($false = ((c @ X1 @ france))) | (((c @ X2 @ X1)) = $true) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f115])).
% 4.04/1.02  thf(f117,plain,(
% 4.04/1.02    ( ! [X2 : reg,X1 : reg] : (($true = (((^[Y0 : reg]: ((c @ Y0 @ (sK1 @ X1)) => (c @ Y0 @ france))) @ X2))) | ($true = (((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ X1)))) & (!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ paris))))))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(pi_proxy_clausification,[],[f104])).
% 4.04/1.02  thf(f118,plain,(
% 4.04/1.02    ( ! [X2 : reg,X1 : reg] : (($true = (((^[Y0 : reg]: ((c @ Y0 @ (sK1 @ X1)) => (c @ Y0 @ france))) @ X2))) | ($true = ((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ paris)))))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(and_proxy_clausification,[],[f117])).
% 4.04/1.02  thf(f119,plain,(
% 4.04/1.02    ( ! [X2 : reg,X1 : reg] : (($true = (((^[Y0 : reg]: ((c @ Y0 @ (sK1 @ X1)) => (c @ Y0 @ france))) @ X2))) | ($true = ((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ X1)))))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(and_proxy_clausification,[],[f117])).
% 4.04/1.02  thf(f120,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($true = (((^[Y0 : reg]: ((c @ Y0 @ (sK1 @ X1)) => (c @ Y0 @ france))) @ X2))) | ($true = (((^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ X1))) @ X3))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(pi_proxy_clausification,[],[f119])).
% 4.04/1.02  thf(f121,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($true = (((c @ X2 @ (sK1 @ X1)) => (c @ X2 @ france)))) | ($true = (((c @ X3 @ (sK2 @ X1)) => (c @ X3 @ X1)))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(beta-eta_normalization,[],[f120])).
% 4.04/1.02  thf(f122,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($false = ((c @ X2 @ (sK1 @ X1)))) | ($true = (((c @ X3 @ (sK2 @ X1)) => (c @ X3 @ X1)))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris))) | ($true = ((c @ X2 @ france)))) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f121])).
% 4.04/1.02  thf(f123,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($false = ((c @ X3 @ (sK2 @ X1)))) | ($false = ((c @ X2 @ (sK1 @ X1)))) | ($true = ((c @ X2 @ france))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris))) | ($true = ((c @ X3 @ X1)))) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f122])).
% 4.04/1.02  thf(f124,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($true = (((^[Y0 : reg]: ((c @ Y0 @ (sK1 @ X1)) => (c @ Y0 @ france))) @ X2))) | ($true = (((^[Y0 : reg]: ((c @ Y0 @ (sK2 @ X1)) => (c @ Y0 @ paris))) @ X3))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(pi_proxy_clausification,[],[f118])).
% 4.04/1.02  thf(f125,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($true = (((c @ X2 @ (sK1 @ X1)) => (c @ X2 @ france)))) | ($true = (((c @ X3 @ (sK2 @ X1)) => (c @ X3 @ paris)))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(beta-eta_normalization,[],[f124])).
% 4.04/1.02  thf(f126,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($false = ((c @ X2 @ (sK1 @ X1)))) | ($true = (((c @ X3 @ (sK2 @ X1)) => (c @ X3 @ paris)))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris))) | ($true = ((c @ X2 @ france)))) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f125])).
% 4.04/1.02  thf(f127,plain,(
% 4.04/1.02    ( ! [X2 : reg,X3 : reg,X1 : reg] : (($false = ((c @ X3 @ (sK2 @ X1)))) | ($false = ((c @ X2 @ (sK1 @ X1)))) | ($true = ((c @ X3 @ paris))) | ($true = ((c @ X2 @ france))) | ($false = ((c @ X1 @ france))) | ($false = ((c @ X1 @ paris)))) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f126])).
% 4.04/1.02  thf(f128,plain,(
% 4.04/1.02    ($true = (((c @ spain @ france) & (~ (?? @ reg @ (^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ spain)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ france)))))))))))),
% 4.04/1.02    inference(beta-eta_normalization,[],[f74])).
% 4.04/1.02  thf(f129,plain,(
% 4.04/1.02    ($true = ((~ (?? @ reg @ (^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ spain)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ france))))))))))),
% 4.04/1.02    inference(and_proxy_clausification,[],[f128])).
% 4.04/1.02  thf(f130,plain,(
% 4.04/1.02    ($true = ((c @ spain @ france)))),
% 4.04/1.02    inference(and_proxy_clausification,[],[f128])).
% 4.04/1.02  thf(f131,plain,(
% 4.04/1.02    ($false = ((?? @ reg @ (^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ spain)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ france)))))))))),
% 4.04/1.02    inference(not_proxy_clausification,[],[f129])).
% 4.04/1.02  thf(f132,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = (((^[Y0 : reg]: ((!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ spain)))) & (!! @ reg @ (^[Y1 : reg]: ((c @ Y1 @ Y0) => (c @ Y1 @ france)))))) @ X1)))) )),
% 4.04/1.02    inference(pi_proxy_clausification,[],[f131])).
% 4.04/1.02  thf(f133,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = (((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ X1) => (c @ Y0 @ spain)))) & (!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ X1) => (c @ Y0 @ france)))))))) )),
% 4.04/1.02    inference(beta-eta_normalization,[],[f132])).
% 4.04/1.02  thf(f134,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = ((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ X1) => (c @ Y0 @ france)))))) | ($false = ((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ X1) => (c @ Y0 @ spain))))))) )),
% 4.04/1.02    inference(and_proxy_clausification,[],[f133])).
% 4.04/1.02  thf(f135,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = (((^[Y0 : reg]: ((c @ Y0 @ X1) => (c @ Y0 @ france))) @ (sK3 @ X1)))) | ($false = ((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ X1) => (c @ Y0 @ spain))))))) )),
% 4.04/1.02    inference(sigma_proxy_clausification,[],[f134])).
% 4.04/1.02  thf(f136,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = (((^[Y0 : reg]: ((c @ Y0 @ X1) => (c @ Y0 @ france))) @ (sK3 @ X1)))) | ($false = (((^[Y0 : reg]: ((c @ Y0 @ X1) => (c @ Y0 @ spain))) @ (sK4 @ X1))))) )),
% 4.04/1.02    inference(sigma_proxy_clausification,[],[f135])).
% 4.04/1.02  thf(f137,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = (((c @ (sK3 @ X1) @ X1) => (c @ (sK3 @ X1) @ france)))) | ($false = (((c @ (sK4 @ X1) @ X1) => (c @ (sK4 @ X1) @ spain))))) )),
% 4.04/1.02    inference(beta-eta_normalization,[],[f136])).
% 4.04/1.02  thf(f138,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = ((c @ (sK3 @ X1) @ france))) | ($false = (((c @ (sK4 @ X1) @ X1) => (c @ (sK4 @ X1) @ spain))))) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f137])).
% 4.04/1.02  thf(f139,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = ((c @ (sK3 @ X1) @ X1))) | ($false = (((c @ (sK4 @ X1) @ X1) => (c @ (sK4 @ X1) @ spain))))) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f137])).
% 4.04/1.02  thf(f140,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = ((c @ (sK3 @ X1) @ X1))) | ($false = ((c @ (sK4 @ X1) @ spain)))) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f139])).
% 4.04/1.02  thf(f141,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = ((c @ (sK4 @ X1) @ X1))) | ($true = ((c @ (sK3 @ X1) @ X1)))) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f139])).
% 4.04/1.02  thf(f142,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = ((c @ (sK4 @ X1) @ spain))) | ($false = ((c @ (sK3 @ X1) @ france)))) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f138])).
% 4.04/1.02  thf(f143,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = ((c @ (sK3 @ X1) @ france))) | ($true = ((c @ (sK4 @ X1) @ X1)))) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f138])).
% 4.04/1.02  thf(f144,plain,(
% 4.04/1.02    ($true = ((((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ catalunya) => (c @ Y0 @ spain)))) & (~ (!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ spain) => (c @ Y0 @ catalunya)))))) & (?? @ reg @ (^[Y0 : reg]: (((c @ Y0 @ catalunya) & (~ (?? @ reg @ (^[Y1 : reg]: ((!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ Y0)))) & (!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ catalunya))))))))) & ((c @ Y0 @ spain) & (~ (?? @ reg @ (^[Y1 : reg]: ((!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ Y0)))) & (!! @ reg @ (^[Y2 : reg]: ((c @ Y2 @ Y1) => (c @ Y2 @ spain)))))))))))))))),
% 4.04/1.02    inference(beta-eta_normalization,[],[f73])).
% 4.04/1.02  thf(f146,plain,(
% 4.04/1.02    ($true = (((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ catalunya) => (c @ Y0 @ spain)))) & (~ (!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ spain) => (c @ Y0 @ catalunya))))))))),
% 4.04/1.02    inference(and_proxy_clausification,[],[f144])).
% 4.04/1.02  thf(f148,plain,(
% 4.04/1.02    ($true = ((!! @ reg @ (^[Y0 : reg]: ((c @ Y0 @ catalunya) => (c @ Y0 @ spain))))))),
% 4.04/1.02    inference(and_proxy_clausification,[],[f146])).
% 4.04/1.02  thf(f149,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = (((^[Y0 : reg]: ((c @ Y0 @ catalunya) => (c @ Y0 @ spain))) @ X1)))) )),
% 4.04/1.02    inference(pi_proxy_clausification,[],[f148])).
% 4.04/1.02  thf(f150,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($true = (((c @ X1 @ catalunya) => (c @ X1 @ spain))))) )),
% 4.04/1.02    inference(beta-eta_normalization,[],[f149])).
% 4.04/1.02  thf(f151,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = ((c @ X1 @ catalunya))) | ($true = ((c @ X1 @ spain)))) )),
% 4.04/1.02    inference(imp_proxy_clausification,[],[f150])).
% 4.04/1.02  thf(f192,definition,(
% 4.04/1.02    spl11_1 <=> ($true = ((c @ catalunya @ paris)))),
% 4.04/1.02    introduced(definition,[new_symbols(definition,[spl11_1])],[avatar_definition])).
% 4.04/1.02  thf(f194,plain,(
% 4.04/1.02    ($true = ((c @ catalunya @ paris))) | ~spl11_1),
% 4.04/1.02    inference(avatar_component_clause,[],[f192])).
% 4.04/1.02  thf(f196,definition,(
% 4.04/1.02    spl11_2 <=> ($true = ((c @ spain @ paris)))),
% 4.04/1.02    introduced(definition,[new_symbols(definition,[spl11_2])],[avatar_definition])).
% 4.04/1.02  thf(f197,plain,(
% 4.04/1.02    ($true != ((c @ spain @ paris))) | spl11_2),
% 4.04/1.02    inference(avatar_component_clause,[],[f196])).
% 4.04/1.02  thf(f198,plain,(
% 4.04/1.02    ($true = ((c @ spain @ paris))) | ~spl11_2),
% 4.04/1.02    inference(avatar_component_clause,[],[f196])).
% 4.04/1.02  thf(f199,plain,(
% 4.04/1.02    spl11_1 | spl11_2),
% 4.04/1.02    inference(avatar_split_clause,[],[f79,f196,f192])).
% 4.04/1.02  thf(f208,plain,(
% 4.04/1.02    ( ! [X0 : reg,X1 : reg] : (($true != $true) | (((c @ X1 @ X0)) = $true) | (((c @ X0 @ X1)) = $false)) )),
% 4.04/1.02    inference(constrained_superposition,[],[f50,f65])).
% 4.04/1.02  thf(f209,plain,(
% 4.04/1.02    ( ! [X0 : reg,X1 : reg] : ((((c @ X1 @ X0)) = $true) | (((c @ X0 @ X1)) = $false)) )),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f208])).
% 4.04/1.02  thf(f249,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($true = $false) | ($false = ((c @ catalunya @ X0))) | ($true = ((c @ X0 @ spain)))) )),
% 4.04/1.02    inference(constrained_superposition,[],[f209,f151])).
% 4.04/1.02  thf(f251,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($false = ((c @ catalunya @ X0))) | ($true = ((c @ X0 @ spain)))) )),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f249])).
% 4.04/1.02  thf(f621,plain,(
% 4.04/1.02    ( ! [X0 : reg,X1 : reg] : (($true = $false) | ($false = ((c @ X0 @ (sK2 @ spain)))) | ($false = ((c @ X1 @ (sK1 @ spain)))) | ($false = ((c @ spain @ paris))) | ($true = ((c @ X1 @ spain))) | ($true = ((c @ X0 @ spain)))) )),
% 4.04/1.02    inference(constrained_superposition,[],[f130,f112])).
% 4.04/1.02  thf(f624,plain,(
% 4.04/1.02    ( ! [X0 : reg,X1 : reg] : (($false = ((c @ X0 @ (sK2 @ spain)))) | ($false = ((c @ X1 @ (sK1 @ spain)))) | ($false = ((c @ spain @ paris))) | ($true = ((c @ X1 @ spain))) | ($true = ((c @ X0 @ spain)))) )),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f621])).
% 4.04/1.02  thf(f674,plain,(
% 4.04/1.02    ( ! [X0 : reg,X1 : reg] : (($true = $false) | ($false = ((c @ X0 @ (sK2 @ spain)))) | ($false = ((c @ X1 @ (sK1 @ spain)))) | ($true = ((c @ X1 @ spain))) | ($true = ((c @ X0 @ spain)))) ) | ~spl11_2),
% 4.04/1.02    inference(forward_demodulation,[],[f624,f198])).
% 4.04/1.02  thf(f675,plain,(
% 4.04/1.02    ( ! [X0 : reg,X1 : reg] : (($false = ((c @ X0 @ (sK2 @ spain)))) | ($false = ((c @ X1 @ (sK1 @ spain)))) | ($true = ((c @ X1 @ spain))) | ($true = ((c @ X0 @ spain)))) ) | ~spl11_2),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f674])).
% 4.04/1.02  thf(f721,definition,(
% 4.04/1.02    spl11_19 <=> ! [X1 : reg] : (($false = ((c @ X1 @ (sK1 @ spain)))) | ($true = ((c @ X1 @ spain))))),
% 4.04/1.02    introduced(definition,[new_symbols(definition,[spl11_19])],[avatar_definition])).
% 4.04/1.02  thf(f722,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = ((c @ X1 @ (sK1 @ spain)))) | ($true = ((c @ X1 @ spain)))) ) | ~spl11_19),
% 4.04/1.02    inference(avatar_component_clause,[],[f721])).
% 4.04/1.02  thf(f724,definition,(
% 4.04/1.02    spl11_20 <=> ! [X0 : reg] : (($false = ((c @ X0 @ (sK2 @ spain)))) | ($true = ((c @ X0 @ spain))))),
% 4.04/1.02    introduced(definition,[new_symbols(definition,[spl11_20])],[avatar_definition])).
% 4.04/1.02  thf(f725,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($false = ((c @ X0 @ (sK2 @ spain)))) | ($true = ((c @ X0 @ spain)))) ) | ~spl11_20),
% 4.04/1.02    inference(avatar_component_clause,[],[f724])).
% 4.04/1.02  thf(f726,plain,(
% 4.04/1.02    spl11_19 | spl11_20 | ~spl11_2),
% 4.04/1.02    inference(avatar_split_clause,[],[f675,f196,f724,f721])).
% 4.04/1.02  thf(f738,plain,(
% 4.04/1.02    ($true = $false) | ($true = ((c @ paris @ spain))) | ~spl11_1),
% 4.04/1.02    inference(constrained_superposition,[],[f251,f194])).
% 4.04/1.02  thf(f739,plain,(
% 4.04/1.02    ($true = ((c @ paris @ spain))) | ~spl11_1),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f738])).
% 4.04/1.02  thf(f758,plain,(
% 4.04/1.02    ($true = $false) | ($true = ((c @ spain @ paris))) | ~spl11_1),
% 4.04/1.02    inference(constrained_superposition,[],[f739,f209])).
% 4.04/1.02  thf(f763,plain,(
% 4.04/1.02    ($true = ((c @ spain @ paris))) | ~spl11_1),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f758])).
% 4.04/1.02  thf(f768,plain,(
% 4.04/1.02    $false | (~spl11_1 | spl11_2)),
% 4.04/1.02    inference(forward_subsumption_resolution,[],[f763,f197])).
% 4.04/1.02  thf(f769,plain,(
% 4.04/1.02    ~spl11_1 | spl11_2),
% 4.04/1.02    inference(avatar_contradiction_clause,[],[f768])).
% 4.04/1.02  thf(f775,plain,(
% 4.04/1.02    ($true = $false) | ($true = ((c @ (sK4 @ (sK1 @ spain)) @ spain))) | ($false = ((c @ (sK3 @ (sK1 @ spain)) @ france))) | ~spl11_19),
% 4.04/1.02    inference(constrained_superposition,[],[f722,f143])).
% 4.04/1.02  thf(f776,plain,(
% 4.04/1.02    ($true = $false) | ($true = ((c @ (sK4 @ (sK1 @ spain)) @ spain))) | ($true = ((c @ (sK3 @ (sK1 @ spain)) @ (sK1 @ spain)))) | ~spl11_19),
% 4.04/1.02    inference(constrained_superposition,[],[f722,f141])).
% 4.04/1.02  thf(f790,plain,(
% 4.04/1.02    ($true = ((c @ (sK4 @ (sK1 @ spain)) @ spain))) | ($true = ((c @ (sK3 @ (sK1 @ spain)) @ (sK1 @ spain)))) | ~spl11_19),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f776])).
% 4.04/1.02  thf(f791,plain,(
% 4.04/1.02    ($true = ((c @ (sK4 @ (sK1 @ spain)) @ spain))) | ($false = ((c @ (sK3 @ (sK1 @ spain)) @ france))) | ~spl11_19),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f775])).
% 4.04/1.02  thf(f796,definition,(
% 4.04/1.02    spl11_23 <=> ($true = ((c @ (sK4 @ (sK1 @ spain)) @ spain)))),
% 4.04/1.02    introduced(definition,[new_symbols(definition,[spl11_23])],[avatar_definition])).
% 4.04/1.02  thf(f798,plain,(
% 4.04/1.02    ($true = ((c @ (sK4 @ (sK1 @ spain)) @ spain))) | ~spl11_23),
% 4.04/1.02    inference(avatar_component_clause,[],[f796])).
% 4.04/1.02  thf(f800,definition,(
% 4.04/1.02    spl11_24 <=> ($true = ((c @ (sK3 @ (sK1 @ spain)) @ (sK1 @ spain))))),
% 4.04/1.02    introduced(definition,[new_symbols(definition,[spl11_24])],[avatar_definition])).
% 4.04/1.02  thf(f802,plain,(
% 4.04/1.02    ($true = ((c @ (sK3 @ (sK1 @ spain)) @ (sK1 @ spain)))) | ~spl11_24),
% 4.04/1.02    inference(avatar_component_clause,[],[f800])).
% 4.04/1.02  thf(f805,definition,(
% 4.04/1.02    spl11_25 <=> ($false = ((c @ (sK3 @ (sK1 @ spain)) @ france)))),
% 4.04/1.02    introduced(definition,[new_symbols(definition,[spl11_25])],[avatar_definition])).
% 4.04/1.02  thf(f807,plain,(
% 4.04/1.02    ($false = ((c @ (sK3 @ (sK1 @ spain)) @ france))) | ~spl11_25),
% 4.04/1.02    inference(avatar_component_clause,[],[f805])).
% 4.04/1.02  thf(f818,plain,(
% 4.04/1.02    spl11_24 | spl11_23 | ~spl11_19),
% 4.04/1.02    inference(avatar_split_clause,[],[f790,f721,f796,f800])).
% 4.04/1.02  thf(f819,plain,(
% 4.04/1.02    spl11_25 | spl11_23 | ~spl11_19),
% 4.04/1.02    inference(avatar_split_clause,[],[f791,f721,f796,f805])).
% 4.04/1.02  thf(f824,plain,(
% 4.04/1.02    ($true = $false) | ($true = ((c @ (sK4 @ (sK2 @ spain)) @ spain))) | ($false = ((c @ (sK3 @ (sK2 @ spain)) @ france))) | ~spl11_20),
% 4.04/1.02    inference(constrained_superposition,[],[f725,f143])).
% 4.04/1.02  thf(f825,plain,(
% 4.04/1.02    ($true = $false) | ($true = ((c @ (sK4 @ (sK2 @ spain)) @ spain))) | ($true = ((c @ (sK3 @ (sK2 @ spain)) @ (sK2 @ spain)))) | ~spl11_20),
% 4.04/1.02    inference(constrained_superposition,[],[f725,f141])).
% 4.04/1.02  thf(f839,plain,(
% 4.04/1.02    ($true = ((c @ (sK4 @ (sK2 @ spain)) @ spain))) | ($true = ((c @ (sK3 @ (sK2 @ spain)) @ (sK2 @ spain)))) | ~spl11_20),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f825])).
% 4.04/1.02  thf(f840,plain,(
% 4.04/1.02    ($true = ((c @ (sK4 @ (sK2 @ spain)) @ spain))) | ($false = ((c @ (sK3 @ (sK2 @ spain)) @ france))) | ~spl11_20),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f824])).
% 4.04/1.02  thf(f845,definition,(
% 4.04/1.02    spl11_28 <=> ($true = ((c @ (sK4 @ (sK2 @ spain)) @ spain)))),
% 4.04/1.02    introduced(definition,[new_symbols(definition,[spl11_28])],[avatar_definition])).
% 4.04/1.02  thf(f847,plain,(
% 4.04/1.02    ($true = ((c @ (sK4 @ (sK2 @ spain)) @ spain))) | ~spl11_28),
% 4.04/1.02    inference(avatar_component_clause,[],[f845])).
% 4.04/1.02  thf(f849,definition,(
% 4.04/1.02    spl11_29 <=> ($true = ((c @ (sK3 @ (sK2 @ spain)) @ (sK2 @ spain))))),
% 4.04/1.02    introduced(definition,[new_symbols(definition,[spl11_29])],[avatar_definition])).
% 4.04/1.02  thf(f850,plain,(
% 4.04/1.02    ($true != ((c @ (sK3 @ (sK2 @ spain)) @ (sK2 @ spain)))) | spl11_29),
% 4.04/1.02    inference(avatar_component_clause,[],[f849])).
% 4.04/1.02  thf(f851,plain,(
% 4.04/1.02    ($true = ((c @ (sK3 @ (sK2 @ spain)) @ (sK2 @ spain)))) | ~spl11_29),
% 4.04/1.02    inference(avatar_component_clause,[],[f849])).
% 4.04/1.02  thf(f854,definition,(
% 4.04/1.02    spl11_30 <=> ($false = ((c @ (sK3 @ (sK2 @ spain)) @ france)))),
% 4.04/1.02    introduced(definition,[new_symbols(definition,[spl11_30])],[avatar_definition])).
% 4.04/1.02  thf(f856,plain,(
% 4.04/1.02    ($false = ((c @ (sK3 @ (sK2 @ spain)) @ france))) | ~spl11_30),
% 4.04/1.02    inference(avatar_component_clause,[],[f854])).
% 4.04/1.02  thf(f863,definition,(
% 4.04/1.02    spl11_32 <=> ($false = ((c @ (sK4 @ (sK2 @ spain)) @ spain)))),
% 4.04/1.02    introduced(definition,[new_symbols(definition,[spl11_32])],[avatar_definition])).
% 4.04/1.02  thf(f864,plain,(
% 4.04/1.02    ($false != ((c @ (sK4 @ (sK2 @ spain)) @ spain))) | spl11_32),
% 4.04/1.02    inference(avatar_component_clause,[],[f863])).
% 4.04/1.02  thf(f865,plain,(
% 4.04/1.02    ($false = ((c @ (sK4 @ (sK2 @ spain)) @ spain))) | ~spl11_32),
% 4.04/1.02    inference(avatar_component_clause,[],[f863])).
% 4.04/1.02  thf(f867,plain,(
% 4.04/1.02    spl11_29 | spl11_28 | ~spl11_20),
% 4.04/1.02    inference(avatar_split_clause,[],[f839,f724,f845,f849])).
% 4.04/1.02  thf(f868,plain,(
% 4.04/1.02    spl11_30 | spl11_28 | ~spl11_20),
% 4.04/1.02    inference(avatar_split_clause,[],[f840,f724,f845,f854])).
% 4.04/1.02  thf(f922,plain,(
% 4.04/1.02    ($true = $false) | ($false = ((c @ (sK3 @ (sK1 @ spain)) @ france))) | ~spl11_23),
% 4.04/1.02    inference(constrained_superposition,[],[f142,f798])).
% 4.04/1.02  thf(f923,plain,(
% 4.04/1.02    ($false = ((c @ (sK3 @ (sK1 @ spain)) @ france))) | ~spl11_23),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f922])).
% 4.04/1.02  thf(f928,plain,(
% 4.04/1.02    spl11_25 | ~spl11_23),
% 4.04/1.02    inference(avatar_split_clause,[],[f923,f796,f805])).
% 4.04/1.02  thf(f2103,plain,(
% 4.04/1.02    ( ! [X0 : reg,X1 : reg] : (($true = $false) | ($false = ((c @ X0 @ (sK2 @ spain)))) | ($false = ((c @ X1 @ (sK1 @ spain)))) | ($true = ((c @ X1 @ france))) | ($false = ((c @ spain @ paris))) | ($true = ((c @ X0 @ spain)))) )),
% 4.04/1.02    inference(constrained_superposition,[],[f130,f123])).
% 4.04/1.02  thf(f2109,plain,(
% 4.04/1.02    ( ! [X0 : reg,X1 : reg] : (($false = ((c @ X0 @ (sK2 @ spain)))) | ($false = ((c @ X1 @ (sK1 @ spain)))) | ($true = ((c @ X1 @ france))) | ($false = ((c @ spain @ paris))) | ($true = ((c @ X0 @ spain)))) )),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f2103])).
% 4.04/1.02  thf(f2217,plain,(
% 4.04/1.02    ( ! [X0 : reg,X1 : reg] : (($true = $false) | ($false = ((c @ X0 @ (sK2 @ spain)))) | ($false = ((c @ X1 @ (sK1 @ spain)))) | ($true = ((c @ X1 @ france))) | ($true = ((c @ X0 @ spain)))) ) | ~spl11_2),
% 4.04/1.02    inference(forward_demodulation,[],[f2109,f198])).
% 4.04/1.02  thf(f2218,plain,(
% 4.04/1.02    ( ! [X0 : reg,X1 : reg] : (($false = ((c @ X0 @ (sK2 @ spain)))) | ($false = ((c @ X1 @ (sK1 @ spain)))) | ($true = ((c @ X1 @ france))) | ($true = ((c @ X0 @ spain)))) ) | ~spl11_2),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f2217])).
% 4.04/1.02  thf(f2249,definition,(
% 4.04/1.02    spl11_60 <=> ! [X1 : reg] : (($false = ((c @ X1 @ (sK1 @ spain)))) | ($true = ((c @ X1 @ france))))),
% 4.04/1.02    introduced(definition,[new_symbols(definition,[spl11_60])],[avatar_definition])).
% 4.04/1.02  thf(f2250,plain,(
% 4.04/1.02    ( ! [X1 : reg] : (($false = ((c @ X1 @ (sK1 @ spain)))) | ($true = ((c @ X1 @ france)))) ) | ~spl11_60),
% 4.04/1.02    inference(avatar_component_clause,[],[f2249])).
% 4.04/1.02  thf(f2251,plain,(
% 4.04/1.02    spl11_60 | spl11_20 | ~spl11_2),
% 4.04/1.02    inference(avatar_split_clause,[],[f2218,f196,f724,f2249])).
% 4.04/1.02  thf(f2326,plain,(
% 4.04/1.02    ($true != $true) | ($true = ((c @ spain @ (sK4 @ (sK2 @ spain))))) | ~spl11_28),
% 4.04/1.02    inference(constrained_superposition,[],[f50,f847])).
% 4.04/1.02  thf(f2327,plain,(
% 4.04/1.02    ($true = $false) | ($false = ((c @ (sK3 @ (sK2 @ spain)) @ france))) | ~spl11_28),
% 4.04/1.02    inference(constrained_superposition,[],[f142,f847])).
% 4.04/1.02  thf(f2328,plain,(
% 4.04/1.02    ($false = ((c @ (sK3 @ (sK2 @ spain)) @ france))) | ~spl11_28),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f2327])).
% 4.04/1.02  thf(f2329,plain,(
% 4.04/1.02    ($true = ((c @ spain @ (sK4 @ (sK2 @ spain))))) | ~spl11_28),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f2326])).
% 4.04/1.02  thf(f2333,plain,(
% 4.04/1.02    spl11_30 | ~spl11_28),
% 4.04/1.02    inference(avatar_split_clause,[],[f2328,f845,f854])).
% 4.04/1.02  thf(f2358,plain,(
% 4.04/1.02    ($true = $false) | ($false = ((c @ (sK4 @ (sK1 @ spain)) @ spain))) | ($true = ((c @ (sK3 @ (sK1 @ spain)) @ france))) | ~spl11_60),
% 4.04/1.02    inference(constrained_superposition,[],[f140,f2250])).
% 4.04/1.02  thf(f2369,plain,(
% 4.04/1.02    ($false = ((c @ (sK4 @ (sK1 @ spain)) @ spain))) | ($true = ((c @ (sK3 @ (sK1 @ spain)) @ france))) | ~spl11_60),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f2358])).
% 4.04/1.02  thf(f2386,plain,(
% 4.04/1.02    ($true = $false) | ($true = ((c @ (sK3 @ (sK1 @ spain)) @ france))) | (~spl11_23 | ~spl11_60)),
% 4.04/1.02    inference(forward_demodulation,[],[f2369,f798])).
% 4.04/1.02  thf(f2387,plain,(
% 4.04/1.02    ($true = ((c @ (sK3 @ (sK1 @ spain)) @ france))) | (~spl11_23 | ~spl11_60)),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f2386])).
% 4.04/1.02  thf(f2391,plain,(
% 4.04/1.02    ($true = $false) | (~spl11_23 | ~spl11_25 | ~spl11_60)),
% 4.04/1.02    inference(forward_demodulation,[],[f2387,f807])).
% 4.04/1.02  thf(f2392,plain,(
% 4.04/1.02    $false | (~spl11_23 | ~spl11_25 | ~spl11_60)),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f2391])).
% 4.04/1.02  thf(f2393,plain,(
% 4.04/1.02    ~spl11_23 | ~spl11_25 | ~spl11_60),
% 4.04/1.02    inference(avatar_contradiction_clause,[],[f2392])).
% 4.04/1.02  thf(f2464,plain,(
% 4.04/1.02    ($true = $false) | ($false = ((c @ (sK3 @ (sK2 @ spain)) @ paris))) | ~spl11_30),
% 4.04/1.02    inference(constrained_superposition,[],[f87,f856])).
% 4.04/1.02  thf(f2465,plain,(
% 4.04/1.02    ($false = ((c @ (sK3 @ (sK2 @ spain)) @ paris))) | ~spl11_30),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f2464])).
% 4.04/1.02  thf(f2491,plain,(
% 4.04/1.02    ($true = $false) | ($false = ((c @ spain @ (sK4 @ (sK2 @ spain))))) | ~spl11_32),
% 4.04/1.02    inference(constrained_superposition,[],[f209,f865])).
% 4.04/1.02  thf(f2495,plain,(
% 4.04/1.02    ($false = ((c @ spain @ (sK4 @ (sK2 @ spain))))) | ~spl11_32),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f2491])).
% 4.04/1.02  thf(f2519,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($true = $false) | ($false = ((c @ X0 @ (sK1 @ spain)))) | ($true = ((c @ (sK3 @ (sK2 @ spain)) @ paris))) | ($false = ((c @ spain @ france))) | ($true = ((c @ X0 @ spain))) | ($false = ((c @ spain @ paris)))) ) | ~spl11_29),
% 4.04/1.02    inference(constrained_superposition,[],[f116,f851])).
% 4.04/1.02  thf(f2524,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($false = ((c @ X0 @ (sK1 @ spain)))) | ($true = ((c @ (sK3 @ (sK2 @ spain)) @ paris))) | ($false = ((c @ spain @ france))) | ($true = ((c @ X0 @ spain))) | ($false = ((c @ spain @ paris)))) ) | ~spl11_29),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f2519])).
% 4.04/1.02  thf(f2914,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($true = $false) | ($false = ((c @ X0 @ (sK1 @ spain)))) | ($true = ((c @ (sK3 @ (sK2 @ spain)) @ paris))) | ($true = ((c @ X0 @ france))) | ($false = ((c @ spain @ france))) | ($false = ((c @ spain @ paris)))) ) | ~spl11_29),
% 4.04/1.02    inference(constrained_superposition,[],[f851,f127])).
% 4.04/1.02  thf(f2979,plain,(
% 4.04/1.02    ( ! [X0 : reg,X1 : reg] : (($true = $false) | ($false = ((c @ X0 @ (sK2 @ spain)))) | ($false = ((c @ X1 @ (sK1 @ spain)))) | ($true = ((c @ X0 @ paris))) | ($true = ((c @ X1 @ france))) | ($false = ((c @ spain @ paris)))) )),
% 4.04/1.02    inference(constrained_superposition,[],[f130,f127])).
% 4.04/1.02  thf(f2985,plain,(
% 4.04/1.02    ( ! [X0 : reg,X1 : reg] : (($false = ((c @ X0 @ (sK2 @ spain)))) | ($false = ((c @ X1 @ (sK1 @ spain)))) | ($true = ((c @ X0 @ paris))) | ($true = ((c @ X1 @ france))) | ($false = ((c @ spain @ paris)))) )),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f2979])).
% 4.04/1.02  thf(f3051,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($false = ((c @ X0 @ (sK1 @ spain)))) | ($true = ((c @ (sK3 @ (sK2 @ spain)) @ paris))) | ($true = ((c @ X0 @ france))) | ($false = ((c @ spain @ france))) | ($false = ((c @ spain @ paris)))) ) | ~spl11_29),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f2914])).
% 4.04/1.02  thf(f3141,plain,(
% 4.04/1.02    ( ! [X0 : reg,X1 : reg] : (($true = $false) | ($false = ((c @ X0 @ (sK2 @ spain)))) | ($false = ((c @ X1 @ (sK1 @ spain)))) | ($true = ((c @ X0 @ paris))) | ($true = ((c @ X1 @ france)))) ) | ~spl11_2),
% 4.04/1.02    inference(forward_demodulation,[],[f2985,f198])).
% 4.04/1.02  thf(f3142,plain,(
% 4.04/1.02    ( ! [X0 : reg,X1 : reg] : (($false = ((c @ X0 @ (sK2 @ spain)))) | ($false = ((c @ X1 @ (sK1 @ spain)))) | ($true = ((c @ X0 @ paris))) | ($true = ((c @ X1 @ france)))) ) | ~spl11_2),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f3141])).
% 4.04/1.02  thf(f3153,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($true = $false) | ($false = ((c @ X0 @ (sK1 @ spain)))) | ($true = ((c @ X0 @ france))) | ($false = ((c @ spain @ france))) | ($false = ((c @ spain @ paris)))) ) | (~spl11_29 | ~spl11_30)),
% 4.04/1.02    inference(forward_demodulation,[],[f3051,f2465])).
% 4.04/1.02  thf(f3154,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($false = ((c @ X0 @ (sK1 @ spain)))) | ($true = ((c @ X0 @ france))) | ($false = ((c @ spain @ france))) | ($false = ((c @ spain @ paris)))) ) | (~spl11_29 | ~spl11_30)),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f3153])).
% 4.04/1.02  thf(f3158,definition,(
% 4.04/1.02    spl11_71 <=> ! [X0 : reg] : (($false = ((c @ X0 @ (sK2 @ spain)))) | ($true = ((c @ X0 @ paris))))),
% 4.04/1.02    introduced(definition,[new_symbols(definition,[spl11_71])],[avatar_definition])).
% 4.04/1.02  thf(f3159,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($false = ((c @ X0 @ (sK2 @ spain)))) | ($true = ((c @ X0 @ paris)))) ) | ~spl11_71),
% 4.04/1.02    inference(avatar_component_clause,[],[f3158])).
% 4.04/1.02  thf(f3160,plain,(
% 4.04/1.02    spl11_60 | spl11_71 | ~spl11_2),
% 4.04/1.02    inference(avatar_split_clause,[],[f3142,f196,f3158,f2249])).
% 4.04/1.02  thf(f3165,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($true = $false) | ($false = ((c @ X0 @ (sK1 @ spain)))) | ($true = ((c @ X0 @ france))) | ($false = ((c @ spain @ paris)))) ) | (~spl11_29 | ~spl11_30)),
% 4.04/1.02    inference(forward_demodulation,[],[f3154,f130])).
% 4.04/1.02  thf(f3166,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($false = ((c @ X0 @ (sK1 @ spain)))) | ($true = ((c @ X0 @ france))) | ($false = ((c @ spain @ paris)))) ) | (~spl11_29 | ~spl11_30)),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f3165])).
% 4.04/1.02  thf(f3169,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($true = $false) | ($false = ((c @ X0 @ (sK1 @ spain)))) | ($true = ((c @ X0 @ france)))) ) | (~spl11_2 | ~spl11_29 | ~spl11_30)),
% 4.04/1.02    inference(forward_demodulation,[],[f3166,f198])).
% 4.04/1.02  thf(f3170,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($false = ((c @ X0 @ (sK1 @ spain)))) | ($true = ((c @ X0 @ france)))) ) | (~spl11_2 | ~spl11_29 | ~spl11_30)),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f3169])).
% 4.04/1.02  thf(f3173,plain,(
% 4.04/1.02    spl11_60 | ~spl11_2 | ~spl11_29 | ~spl11_30),
% 4.04/1.02    inference(avatar_split_clause,[],[f3170,f854,f849,f196,f2249])).
% 4.04/1.02  thf(f3298,plain,(
% 4.04/1.02    ($true = $false) | ($true = ((c @ (sK3 @ (sK1 @ spain)) @ france))) | (~spl11_24 | ~spl11_60)),
% 4.04/1.02    inference(constrained_superposition,[],[f802,f2250])).
% 4.04/1.02  thf(f3329,plain,(
% 4.04/1.02    ($true = ((c @ (sK3 @ (sK1 @ spain)) @ france))) | (~spl11_24 | ~spl11_60)),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f3298])).
% 4.04/1.02  thf(f3344,plain,(
% 4.04/1.02    ($true = $false) | (~spl11_24 | ~spl11_25 | ~spl11_60)),
% 4.04/1.02    inference(forward_demodulation,[],[f3329,f807])).
% 4.04/1.02  thf(f3345,plain,(
% 4.04/1.02    $false | (~spl11_24 | ~spl11_25 | ~spl11_60)),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f3344])).
% 4.04/1.02  thf(f3346,plain,(
% 4.04/1.02    ~spl11_24 | ~spl11_25 | ~spl11_60),
% 4.04/1.02    inference(avatar_contradiction_clause,[],[f3345])).
% 4.04/1.02  thf(f3358,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($true = $false) | ($false = ((c @ X0 @ (sK1 @ spain)))) | ($false = ((c @ spain @ france))) | ($true = ((c @ X0 @ spain))) | ($false = ((c @ spain @ paris)))) ) | (~spl11_29 | ~spl11_30)),
% 4.04/1.02    inference(forward_demodulation,[],[f2524,f2465])).
% 4.04/1.02  thf(f3359,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($false = ((c @ X0 @ (sK1 @ spain)))) | ($false = ((c @ spain @ france))) | ($true = ((c @ X0 @ spain))) | ($false = ((c @ spain @ paris)))) ) | (~spl11_29 | ~spl11_30)),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f3358])).
% 4.04/1.02  thf(f3362,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($true = $false) | ($false = ((c @ X0 @ (sK1 @ spain)))) | ($true = ((c @ X0 @ spain))) | ($false = ((c @ spain @ paris)))) ) | (~spl11_29 | ~spl11_30)),
% 4.04/1.02    inference(forward_demodulation,[],[f3359,f130])).
% 4.04/1.02  thf(f3363,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($false = ((c @ X0 @ (sK1 @ spain)))) | ($true = ((c @ X0 @ spain))) | ($false = ((c @ spain @ paris)))) ) | (~spl11_29 | ~spl11_30)),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f3362])).
% 4.04/1.02  thf(f3366,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($true = $false) | ($false = ((c @ X0 @ (sK1 @ spain)))) | ($true = ((c @ X0 @ spain)))) ) | (~spl11_2 | ~spl11_29 | ~spl11_30)),
% 4.04/1.02    inference(forward_demodulation,[],[f3363,f198])).
% 4.04/1.02  thf(f3367,plain,(
% 4.04/1.02    ( ! [X0 : reg] : (($false = ((c @ X0 @ (sK1 @ spain)))) | ($true = ((c @ X0 @ spain)))) ) | (~spl11_2 | ~spl11_29 | ~spl11_30)),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f3366])).
% 4.04/1.02  thf(f3370,plain,(
% 4.04/1.02    spl11_19 | ~spl11_2 | ~spl11_29 | ~spl11_30),
% 4.04/1.02    inference(avatar_split_clause,[],[f3367,f854,f849,f196,f721])).
% 4.04/1.02  thf(f3374,plain,(
% 4.04/1.02    ($true = $false) | (~spl11_28 | ~spl11_32)),
% 4.04/1.02    inference(forward_demodulation,[],[f2329,f2495])).
% 4.04/1.02  thf(f3375,plain,(
% 4.04/1.02    $false | (~spl11_28 | ~spl11_32)),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f3374])).
% 4.04/1.02  thf(f3376,plain,(
% 4.04/1.02    ~spl11_28 | ~spl11_32),
% 4.04/1.02    inference(avatar_contradiction_clause,[],[f3375])).
% 4.04/1.02  thf(f3397,plain,(
% 4.04/1.02    ($true = $false) | ($true = ((c @ (sK3 @ (sK2 @ spain)) @ paris))) | ($false = ((c @ (sK4 @ (sK2 @ spain)) @ spain))) | ~spl11_71),
% 4.04/1.02    inference(constrained_superposition,[],[f3159,f140])).
% 4.04/1.02  thf(f3431,plain,(
% 4.04/1.02    ($true = ((c @ (sK3 @ (sK2 @ spain)) @ paris))) | ($false = ((c @ (sK4 @ (sK2 @ spain)) @ spain))) | ~spl11_71),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f3397])).
% 4.04/1.02  thf(f3439,plain,(
% 4.04/1.02    ($true = ((c @ (sK3 @ (sK2 @ spain)) @ paris))) | (spl11_32 | ~spl11_71)),
% 4.04/1.02    inference(forward_subsumption_resolution,[],[f3431,f864])).
% 4.04/1.02  thf(f3447,plain,(
% 4.04/1.02    ($true = $false) | (~spl11_30 | spl11_32 | ~spl11_71)),
% 4.04/1.02    inference(forward_demodulation,[],[f3439,f2465])).
% 4.04/1.02  thf(f3448,plain,(
% 4.04/1.02    $false | (~spl11_30 | spl11_32 | ~spl11_71)),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f3447])).
% 4.04/1.02  thf(f3449,plain,(
% 4.04/1.02    ~spl11_30 | spl11_32 | ~spl11_71),
% 4.04/1.02    inference(avatar_contradiction_clause,[],[f3448])).
% 4.04/1.02  thf(f3603,plain,(
% 4.04/1.02    ($true != $true) | ($false = ((c @ (sK4 @ (sK2 @ spain)) @ spain))) | spl11_29),
% 4.04/1.02    inference(constrained_superposition,[],[f850,f140])).
% 4.04/1.02  thf(f3606,plain,(
% 4.04/1.02    ($false = ((c @ (sK4 @ (sK2 @ spain)) @ spain))) | spl11_29),
% 4.04/1.02    inference(trivial_inequality_removal,[],[f3603])).
% 4.04/1.02  thf(f3608,plain,(
% 4.04/1.02    $false | (spl11_29 | spl11_32)),
% 4.04/1.02    inference(forward_subsumption_resolution,[],[f3606,f864])).
% 4.04/1.02  thf(f3609,plain,(
% 4.04/1.02    spl11_29 | spl11_32),
% 4.04/1.02    inference(avatar_contradiction_clause,[],[f3608])).
% 4.04/1.02  cnf(s1, plain, spl11_1 | spl11_2, inference(sat_conversion,[],[f199])).
% 4.04/1.02  cnf(s16, plain, ~spl11_2 | spl11_19 | spl11_20, inference(sat_conversion,[],[f726])).
% 4.04/1.02  cnf(s20, plain, ~spl11_1 | spl11_2, inference(sat_conversion,[],[f769])).
% 4.04/1.02  cnf(s24, plain, ~spl11_19 | spl11_23 | spl11_24, inference(sat_conversion,[],[f818])).
% 4.04/1.02  cnf(s25, plain, ~spl11_19 | spl11_23 | spl11_25, inference(sat_conversion,[],[f819])).
% 4.04/1.02  cnf(s30, plain, ~spl11_20 | spl11_28 | spl11_29, inference(sat_conversion,[],[f867])).
% 4.04/1.02  cnf(s31, plain, ~spl11_20 | spl11_28 | spl11_30, inference(sat_conversion,[],[f868])).
% 4.04/1.02  cnf(s33, plain, ~spl11_23 | spl11_25, inference(sat_conversion,[],[f928])).
% 4.04/1.02  cnf(s55, plain, ~spl11_2 | spl11_20 | spl11_60, inference(sat_conversion,[],[f2251])).
% 4.04/1.02  cnf(s60, plain, ~spl11_28 | spl11_30, inference(sat_conversion,[],[f2333])).
% 4.04/1.02  cnf(s64, plain, ~spl11_23 | ~spl11_25 | ~spl11_60, inference(sat_conversion,[],[f2393])).
% 4.04/1.02  cnf(s76, plain, ~spl11_2 | spl11_60 | spl11_71, inference(sat_conversion,[],[f3160])).
% 4.04/1.02  cnf(s78, plain, ~spl11_2 | ~spl11_29 | ~spl11_30 | spl11_60, inference(sat_conversion,[],[f3173])).
% 4.04/1.02  cnf(s81, plain, ~spl11_24 | ~spl11_25 | ~spl11_60, inference(sat_conversion,[],[f3346])).
% 4.04/1.02  cnf(s84, plain, ~spl11_2 | spl11_19 | ~spl11_29 | ~spl11_30, inference(sat_conversion,[],[f3370])).
% 4.04/1.02  cnf(s87, plain, ~spl11_28 | ~spl11_32, inference(sat_conversion,[],[f3376])).
% 4.04/1.02  cnf(s91, plain, ~spl11_30 | spl11_32 | ~spl11_71, inference(sat_conversion,[],[f3449])).
% 4.04/1.02  cnf(s94, plain, spl11_29 | spl11_32, inference(sat_conversion,[],[f3609])).
% 4.04/1.02  cnf(s95, plain, spl11_28 | spl11_19 | ~spl11_2, inference(rat,[],[s84,s30,s31,s16])).
% 4.04/1.02  cnf(s96, plain, spl11_19 | ~spl11_2, inference(rat,[],[s84,s94,s60,s87,s95])).
% 4.04/1.02  cnf(s98, plain, ~spl11_23 | ~spl11_60, inference(rat,[],[s64,s33])).
% 4.04/1.02  cnf(s99, plain, ~spl11_60 | ~spl11_19, inference(rat,[],[s81,s24,s25,s98])).
% 4.04/1.02  cnf(s100, plain, spl11_28 | ~spl11_2, inference(rat,[],[s78,s30,s31,s55,s99,s96])).
% 4.04/1.02  cnf(s101, plain, spl11_60 | ~spl11_2, inference(rat,[],[s91,s60,s87,s100,s76])).
% 4.04/1.02  cnf(s102, plain, ~spl11_2, inference(rat,[],[s101,s99,s96])).
% 4.04/1.02  cnf(s103, plain, ~spl11_1, inference(rat,[],[s20,s102])).
% 4.04/1.02  cnf(s104, plain, $false, inference(rat,[],[s1,s102,s103])).
% 4.04/1.02  thf(f3610,plain,(
% 4.04/1.02    $false),
% 4.04/1.02    inference(avatar_sat_refutation,[],[s104])).
% 4.04/1.02  % SZS output end Proof for theBenchmark
% 4.04/1.02  % (469228)------------------------------
% 4.04/1.02  % (469228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/1.02  % (469228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/1.02  % (469228)CaDiCaL version: 2.1.3
% 4.04/1.02  % (469228)Termination reason: Refutation
% 4.04/1.02  % (469228)Time elapsed: 0.194 s
% 4.04/1.02  % (469228)Peak memory usage: 14 MB
% 4.04/1.02  % (469228)Instructions burned: 422 (million)
% 4.04/1.02  % (469175)Success in time 0.794 s
% 4.04/1.02  % Vampire exiting
%------------------------------------------------------------------------------