%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU218+3 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Tue Jul 19 14:35:08 EDT 2022 % Result : Theorem 48.79s 48.98s % Output : Refutation 49.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SEU218+3 : TPTP v8.1.0. Released v3.2.0. % 0.03/0.12 % Command : run_spass %d %s % 0.11/0.32 % Computer : n016.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 600 % 0.11/0.32 % DateTime : Mon Jun 20 04:49:09 EDT 2022 % 0.11/0.32 % CPUTime : % 48.79/48.98 % 48.79/48.98 SPASS V 3.9 % 48.79/48.98 SPASS beiseite: Proof found. % 48.79/48.98 % SZS status Theorem % 48.79/48.98 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 48.79/48.98 SPASS derived 23639 clauses, backtracked 972 clauses, performed 14 splits and kept 14114 clauses. % 48.79/48.98 SPASS allocated 126363 KBytes. % 48.79/48.98 SPASS spent 0:0:48.62 on the problem. % 48.79/48.98 0:00:00.04 for the input. % 48.79/48.98 0:00:00.07 for the FLOTTER CNF translation. % 48.79/48.98 0:00:00.38 for inferences. % 48.79/48.98 0:00:02.52 for the backtracking. % 48.79/48.98 0:0:45.33 for the reduction. % 48.79/48.98 % 48.79/48.98 % 48.79/48.98 Here is a proof with depth 7, length 326 : % 48.79/48.98 % SZS output start Refutation % 48.79/48.98 1[0:Inp] || -> relation(skc15)*. % 48.79/48.98 2[0:Inp] || -> relation(skc14)*. % 48.79/48.98 3[0:Inp] || -> function(skc14)*. % 48.79/48.98 4[0:Inp] || -> one_to_one(skc14)*. % 48.79/48.98 5[0:Inp] || -> function(skc15)*. % 48.79/48.98 52[0:Inp] relation(u) || -> equal(relation_inverse(relation_inverse(u)),u)**. % 48.79/48.98 55[0:Inp] || -> equal(relation_rng(skc14),relation_dom(skc15)) equal(function_inverse(skc14),skc15)**. % 48.79/48.98 56[0:Inp] || -> SkP0(skc15,u,skc14,v)* equal(function_inverse(skc14),skc15). % 48.79/48.98 57[0:Inp] || -> in(u,relation_rng(v)) SkP0(w,x,v,u)*. % 48.79/48.98 63[0:Inp] relation(u) || -> equal(relation_dom(relation_inverse(u)),relation_rng(u))**. % 48.79/48.98 64[0:Inp] relation(u) || -> equal(relation_rng(relation_inverse(u)),relation_dom(u))**. % 48.79/48.98 66[0:Inp] || -> equal(u,apply(v,w)) SkP0(v,u,x,w)*. % 48.79/48.98 68[0:Inp] || in(skc19,relation_rng(skc14))* equal(apply(skc15,skc19),skc18) -> . % 48.79/48.98 76[0:Inp] one_to_one(u) function(u) relation(u) || -> equal(function_inverse(u),relation_inverse(u))**. % 48.79/48.98 77[0:Inp] || in(u,relation_dom(v)) equal(w,apply(v,u)) -> SkP0(x,u,v,w)*. % 48.79/48.98 78[0:Inp] relation(u) || equal(v,relation_dom(u))* in(ordered_pair(w,x),u)*+ -> in(w,v)*. % 48.79/48.98 79[0:Inp] relation(u) || equal(v,relation_rng(u))* in(ordered_pair(w,x),u)*+ -> in(x,v)*. % 48.79/48.98 80[0:Inp] || equal(u,apply(skc14,v))* in(v,relation_dom(skc14))* -> in(u,relation_rng(skc14))* equal(function_inverse(skc14),skc15). % 48.79/48.98 83[0:Inp] relation(u) || in(v,w)* equal(w,relation_dom(u))*+ -> in(ordered_pair(v,skf15(u,v)),u)*. % 48.79/48.98 85[0:Inp] || equal(u,apply(skc14,v))* in(v,relation_dom(skc14))* -> equal(v,apply(skc15,u))* equal(function_inverse(skc14),skc15). % 48.79/48.98 90[0:Inp] || in(u,relation_rng(v)) equal(w,apply(x,u)) SkP0(x,w,v,u)* -> in(w,relation_dom(v)). % 48.79/48.98 91[0:Inp] || equal(function_inverse(skc14),skc15) equal(relation_rng(skc14),relation_dom(skc15)) SkP0(skc15,skc16,skc14,skc17)* -> in(skc18,relation_dom(skc14)). % 48.79/48.98 93[0:Inp] relation(u) relation(v) || equal(u,relation_inverse(v))* in(ordered_pair(w,x),u)*+ -> in(ordered_pair(x,w),v)*. % 48.79/48.98 94[0:Inp] function(u) relation(u) || in(v,relation_dom(u)) in(ordered_pair(v,w),u)* -> equal(w,apply(u,v)). % 48.79/48.98 95[0:Inp] function(u) relation(u) || in(v,relation_dom(u)) equal(w,apply(u,v)) -> in(ordered_pair(v,w),u)*. % 48.79/48.98 96[0:Inp] || in(u,relation_rng(v)) equal(w,apply(x,u)) SkP0(x,w,v,u)* -> equal(u,apply(v,w)). % 48.79/48.98 97[0:Inp] || equal(function_inverse(skc14),skc15) equal(relation_rng(skc14),relation_dom(skc15)) SkP0(skc15,skc16,skc14,skc17)* -> equal(apply(skc14,skc18),skc19). % 48.79/48.98 98[0:Inp] relation(u) relation(v) || -> equal(v,u) in(ordered_pair(skf14(u,v),skf13(u,v)),u)* in(ordered_pair(skf14(u,v),skf13(u,v)),v)*. % 48.79/48.98 99[0:Inp] relation(u) relation(v) || -> equal(u,relation_inverse(v)) in(ordered_pair(skf23(v,u),skf24(v,u)),v)* in(ordered_pair(skf24(v,u),skf23(v,u)),u)*. % 48.79/48.98 101[0:Inp] relation(u) relation(v) || in(ordered_pair(skf23(v,u),skf24(v,u)),v)*+ in(ordered_pair(skf24(v,u),skf23(v,u)),u)* -> equal(u,relation_inverse(v)). % 48.79/48.98 104[0:Rew:55.0,80.2] || equal(u,apply(skc14,v))* in(v,relation_dom(skc14))* -> in(u,relation_dom(skc15))* equal(function_inverse(skc14),skc15). % 48.79/48.98 105[0:Res:5.0,95.1] relation(skc15) || equal(u,apply(skc15,v)) in(v,relation_dom(skc15)) -> in(ordered_pair(v,u),skc15)*. % 48.79/48.98 106[0:Res:5.0,94.1] relation(skc15) || in(ordered_pair(u,v),skc15)* in(u,relation_dom(skc15)) -> equal(v,apply(skc15,u)). % 48.79/48.98 113[0:Res:4.0,76.2] relation(skc14) function(skc14) || -> equal(function_inverse(skc14),relation_inverse(skc14))**. % 48.79/48.98 116[0:Res:3.0,94.1] relation(skc14) || in(ordered_pair(u,v),skc14)* in(u,relation_dom(skc14)) -> equal(v,apply(skc14,u)). % 48.79/48.98 123[0:Res:2.0,101.0] relation(u) || in(ordered_pair(skf24(skc14,u),skf23(skc14,u)),u)* in(ordered_pair(skf23(skc14,u),skf24(skc14,u)),skc14) -> equal(u,relation_inverse(skc14)). % 48.79/48.98 125[0:Res:2.0,99.0] relation(u) || -> equal(u,relation_inverse(skc14)) in(ordered_pair(skf24(skc14,u),skf23(skc14,u)),u)* in(ordered_pair(skf23(skc14,u),skf24(skc14,u)),skc14). % 48.79/48.98 126[0:Res:2.0,98.0] relation(u) || -> equal(skc14,u) in(ordered_pair(skf14(u,skc14),skf13(u,skc14)),u)* in(ordered_pair(skf14(u,skc14),skf13(u,skc14)),skc14)*. % 48.79/48.98 129[0:Res:2.0,93.0] relation(u) || equal(u,relation_inverse(skc14)) in(ordered_pair(v,w),u)*+ -> in(ordered_pair(w,v),skc14)*. % 48.79/48.98 136[0:Res:2.0,83.0] || in(u,v)* equal(v,relation_dom(skc14))+ -> in(ordered_pair(u,skf15(skc14,u)),skc14)*. % 48.79/48.98 138[0:Res:2.0,78.0] || equal(u,relation_dom(skc14)) in(ordered_pair(v,w),skc14)*+ -> in(v,u)*. % 48.79/48.98 139[0:Res:2.0,79.0] || equal(u,relation_rng(skc14)) in(ordered_pair(v,w),skc14)* -> in(w,u)*. % 48.79/48.98 146[0:Res:2.0,63.0] || -> equal(relation_dom(relation_inverse(skc14)),relation_rng(skc14))**. % 48.79/48.98 147[0:Res:2.0,64.0] || -> equal(relation_rng(relation_inverse(skc14)),relation_dom(skc14))**. % 48.79/48.98 148[0:Res:2.0,52.0] || -> equal(relation_inverse(relation_inverse(skc14)),skc14)**. % 48.79/48.98 150[0:Res:2.0,101.1] relation(u) || in(ordered_pair(skf23(u,skc14),skf24(u,skc14)),u)*+ in(ordered_pair(skf24(u,skc14),skf23(u,skc14)),skc14)* -> equal(relation_inverse(u),skc14). % 48.79/48.98 152[0:Res:2.0,99.1] relation(u) || -> equal(relation_inverse(u),skc14) in(ordered_pair(skf23(u,skc14),skf24(u,skc14)),u)* in(ordered_pair(skf24(u,skc14),skf23(u,skc14)),skc14)*. % 48.79/48.98 154[0:Res:2.0,93.1] relation(u) || equal(relation_inverse(u),skc14) in(ordered_pair(v,w),skc14)*+ -> in(ordered_pair(w,v),u)*. % 48.79/48.98 163[0:Res:1.0,93.0] relation(u) || equal(u,relation_inverse(skc15)) in(ordered_pair(v,w),u)* -> in(ordered_pair(w,v),skc15)*. % 48.79/48.98 172[0:Res:1.0,78.0] || equal(u,relation_dom(skc15)) in(ordered_pair(v,w),skc15)*+ -> in(v,u)*. % 48.79/48.98 173[0:Res:1.0,79.0] || equal(u,relation_rng(skc15)) in(ordered_pair(v,w),skc15)* -> in(w,u)*. % 48.79/48.98 198[0:MRR:113.0,113.1,2.0,3.0] || -> equal(function_inverse(skc14),relation_inverse(skc14))**. % 48.79/48.98 199[0:Rew:198.0,97.0] || equal(relation_inverse(skc14),skc15) equal(relation_rng(skc14),relation_dom(skc15)) SkP0(skc15,skc16,skc14,skc17)* -> equal(apply(skc14,skc18),skc19). % 48.79/48.98 200[0:Rew:198.0,91.0] || equal(relation_inverse(skc14),skc15) equal(relation_rng(skc14),relation_dom(skc15)) SkP0(skc15,skc16,skc14,skc17)* -> in(skc18,relation_dom(skc14)). % 48.79/48.98 201[0:Rew:198.0,85.3] || in(u,relation_dom(skc14))* equal(v,apply(skc14,u))* -> equal(u,apply(skc15,v))* equal(relation_inverse(skc14),skc15). % 48.79/48.98 202[0:Rew:198.0,104.3] || in(u,relation_dom(skc14))* equal(v,apply(skc14,u))* -> in(v,relation_dom(skc15))* equal(relation_inverse(skc14),skc15). % 48.79/48.98 203[0:Rew:198.0,55.1] || -> equal(relation_inverse(skc14),skc15)** equal(relation_rng(skc14),relation_dom(skc15)). % 48.79/48.98 204[0:Rew:198.0,56.1] || -> equal(relation_inverse(skc14),skc15) SkP0(skc15,u,skc14,v)*. % 48.79/48.98 211[0:MRR:105.0,1.0] || in(u,relation_dom(skc15)) equal(v,apply(skc15,u)) -> in(ordered_pair(u,v),skc15)*. % 48.79/48.98 212[0:MRR:106.0,1.0] || in(u,relation_dom(skc15)) in(ordered_pair(u,v),skc15)* -> equal(v,apply(skc15,u)). % 48.79/48.98 214[0:MRR:116.0,2.0] || in(u,relation_dom(skc14)) in(ordered_pair(u,v),skc14)* -> equal(v,apply(skc14,u)). % 48.79/48.98 215[0:Res:1.0,123.0] || in(ordered_pair(skf23(skc14,skc15),skf24(skc14,skc15)),skc14) in(ordered_pair(skf24(skc14,skc15),skf23(skc14,skc15)),skc15)* -> equal(relation_inverse(skc14),skc15). % 48.79/48.98 216[0:Res:1.0,150.0] || in(ordered_pair(skf23(skc15,skc14),skf24(skc15,skc14)),skc15) in(ordered_pair(skf24(skc15,skc14),skf23(skc15,skc14)),skc14)* -> equal(relation_inverse(skc15),skc14). % 48.79/48.98 223[0:Res:1.0,125.0] || -> equal(relation_inverse(skc14),skc15) in(ordered_pair(skf23(skc14,skc15),skf24(skc14,skc15)),skc14) in(ordered_pair(skf24(skc14,skc15),skf23(skc14,skc15)),skc15)*. % 48.79/48.98 224[0:Res:1.0,152.0] || -> equal(relation_inverse(skc15),skc14) in(ordered_pair(skf23(skc15,skc14),skf24(skc15,skc14)),skc15) in(ordered_pair(skf24(skc15,skc14),skf23(skc15,skc14)),skc14)*. % 48.79/48.98 227[0:Res:1.0,126.0] || -> equal(skc15,skc14) in(ordered_pair(skf14(skc15,skc14),skf13(skc15,skc14)),skc15)* in(ordered_pair(skf14(skc15,skc14),skf13(skc15,skc14)),skc14). % 48.79/48.98 236[0:Res:1.0,154.0] || equal(relation_inverse(skc15),skc14) in(ordered_pair(u,v),skc14)* -> in(ordered_pair(v,u),skc15)*. % 48.79/48.98 238[0:Res:1.0,129.0] || equal(relation_inverse(skc14),skc15) in(ordered_pair(u,v),skc15)* -> in(ordered_pair(v,u),skc14)*. % 48.79/48.98 243[1:Spt:227.0] || -> equal(skc15,skc14)**. % 48.79/48.98 244[1:Rew:243.0,199.1] || equal(relation_inverse(skc14),skc15) equal(relation_rng(skc14),relation_dom(skc14)) SkP0(skc15,skc16,skc14,skc17)* -> equal(apply(skc14,skc18),skc19). % 48.79/48.98 245[1:Rew:243.0,200.1] || equal(relation_inverse(skc14),skc15) equal(relation_rng(skc14),relation_dom(skc14)) SkP0(skc15,skc16,skc14,skc17)* -> in(skc18,relation_dom(skc14)). % 48.79/48.98 246[1:Rew:243.0,203.1] || -> equal(relation_inverse(skc14),skc15)** equal(relation_rng(skc14),relation_dom(skc14)). % 48.79/48.98 249[1:Rew:243.0,202.2] || in(u,relation_dom(skc14))* equal(v,apply(skc14,u))* -> in(v,relation_dom(skc14))* equal(relation_inverse(skc14),skc15). % 48.79/48.98 260[1:Rew:243.0,216.2] || in(ordered_pair(skf23(skc15,skc14),skf24(skc15,skc14)),skc15) in(ordered_pair(skf24(skc15,skc14),skf23(skc15,skc14)),skc14)* -> equal(relation_inverse(skc14),skc14). % 48.79/48.98 261[1:Rew:243.0,224.0] || -> equal(relation_inverse(skc14),skc14) in(ordered_pair(skf23(skc15,skc14),skf24(skc15,skc14)),skc15) in(ordered_pair(skf24(skc15,skc14),skf23(skc15,skc14)),skc14)*. % 48.79/48.98 262[1:Rew:243.0,236.0] || equal(relation_inverse(skc14),skc14) in(ordered_pair(u,v),skc14)* -> in(ordered_pair(v,u),skc15)*. % 48.79/48.98 277[1:Rew:243.0,201.3] || in(u,relation_dom(skc14))* equal(v,apply(skc14,u))* -> equal(u,apply(skc15,v))* equal(relation_inverse(skc14),skc14). % 48.79/48.98 299[1:Rew:243.0,68.1] || in(skc19,relation_rng(skc14))* equal(apply(skc14,skc19),skc18) -> . % 48.79/48.98 304[1:Rew:243.0,246.0] || -> equal(relation_inverse(skc14),skc14)** equal(relation_rng(skc14),relation_dom(skc14)). % 48.79/48.98 313[1:Rew:243.0,262.2] || equal(relation_inverse(skc14),skc14) in(ordered_pair(u,v),skc14)* -> in(ordered_pair(v,u),skc14)*. % 48.79/48.98 323[1:Rew:243.0,249.3] || in(u,relation_dom(skc14))* equal(v,apply(skc14,u))* -> in(v,relation_dom(skc14))* equal(relation_inverse(skc14),skc14). % 48.79/48.98 328[1:Rew:243.0,277.2] || in(u,relation_dom(skc14))* equal(v,apply(skc14,u))* -> equal(u,apply(skc14,v))* equal(relation_inverse(skc14),skc14). % 48.79/48.98 329[1:Rew:243.0,245.2,243.0,245.0] || equal(relation_inverse(skc14),skc14) equal(relation_rng(skc14),relation_dom(skc14)) SkP0(skc14,skc16,skc14,skc17)* -> in(skc18,relation_dom(skc14)). % 48.79/48.98 330[1:Rew:243.0,244.2,243.0,244.0] || equal(relation_inverse(skc14),skc14) equal(relation_rng(skc14),relation_dom(skc14)) SkP0(skc14,skc16,skc14,skc17)* -> equal(apply(skc14,skc18),skc19). % 48.79/48.98 331[1:Rew:243.0,261.2,243.0,261.1] || -> equal(relation_inverse(skc14),skc14) in(ordered_pair(skf23(skc14,skc14),skf24(skc14,skc14)),skc14) in(ordered_pair(skf24(skc14,skc14),skf23(skc14,skc14)),skc14)*. % 48.79/48.98 334[1:Rew:243.0,260.1,243.0,260.0] || in(ordered_pair(skf23(skc14,skc14),skf24(skc14,skc14)),skc14) in(ordered_pair(skf24(skc14,skc14),skf23(skc14,skc14)),skc14)* -> equal(relation_inverse(skc14),skc14). % 48.79/48.98 463[2:Spt:304.0] || -> equal(relation_inverse(skc14),skc14)**. % 48.79/48.98 468[2:Rew:463.0,147.0] || -> equal(relation_rng(skc14),relation_dom(skc14))**. % 48.79/48.98 474[2:Rew:463.0,330.0] || equal(skc14,skc14) equal(relation_rng(skc14),relation_dom(skc14)) SkP0(skc14,skc16,skc14,skc17)* -> equal(apply(skc14,skc18),skc19). % 48.79/48.98 475[2:Rew:463.0,329.0] || equal(skc14,skc14) equal(relation_rng(skc14),relation_dom(skc14)) SkP0(skc14,skc16,skc14,skc17)* -> in(skc18,relation_dom(skc14)). % 48.79/48.98 476[2:Rew:463.0,313.0] || equal(skc14,skc14) in(ordered_pair(u,v),skc14)* -> in(ordered_pair(v,u),skc14)*. % 48.79/48.98 480[2:Rew:468.0,139.0] || equal(u,relation_dom(skc14)) in(ordered_pair(v,w),skc14)*+ -> in(w,u)*. % 48.79/48.98 482[2:Rew:468.0,299.0] || in(skc19,relation_dom(skc14))* equal(apply(skc14,skc19),skc18) -> . % 48.79/48.98 484[2:Obv:476.0] || in(ordered_pair(u,v),skc14)*+ -> in(ordered_pair(v,u),skc14)*. % 48.79/48.98 485[2:Obv:475.0] || equal(relation_rng(skc14),relation_dom(skc14)) SkP0(skc14,skc16,skc14,skc17)* -> in(skc18,relation_dom(skc14)). % 48.79/48.98 486[2:Rew:468.0,485.0] || equal(relation_dom(skc14),relation_dom(skc14)) SkP0(skc14,skc16,skc14,skc17)* -> in(skc18,relation_dom(skc14)). % 48.79/48.98 487[2:Obv:486.0] || SkP0(skc14,skc16,skc14,skc17)* -> in(skc18,relation_dom(skc14)). % 48.79/48.98 488[2:Obv:474.0] || equal(relation_rng(skc14),relation_dom(skc14)) SkP0(skc14,skc16,skc14,skc17)* -> equal(apply(skc14,skc18),skc19). % 48.79/48.98 489[2:Rew:468.0,488.0] || equal(relation_dom(skc14),relation_dom(skc14)) SkP0(skc14,skc16,skc14,skc17)* -> equal(apply(skc14,skc18),skc19). % 48.79/48.98 490[2:Obv:489.0] || SkP0(skc14,skc16,skc14,skc17)* -> equal(apply(skc14,skc18),skc19). % 48.79/48.98 566[2:Res:57.1,487.0] || -> in(skc17,relation_rng(skc14)) in(skc18,relation_dom(skc14))*. % 48.79/48.98 567[2:Rew:468.0,566.0] || -> in(skc17,relation_dom(skc14)) in(skc18,relation_dom(skc14))*. % 48.79/48.98 589[2:Res:66.1,487.0] || -> equal(apply(skc14,skc17),skc16) in(skc18,relation_dom(skc14))*. % 48.79/48.98 590[3:Spt:589.1] || -> in(skc18,relation_dom(skc14))*. % 48.79/48.98 596[2:Res:57.1,490.0] || -> in(skc17,relation_rng(skc14))* equal(apply(skc14,skc18),skc19). % 48.79/48.98 597[2:Res:66.1,490.0] || -> equal(apply(skc14,skc17),skc16) equal(apply(skc14,skc18),skc19)**. % 48.79/48.98 598[2:Rew:468.0,596.0] || -> in(skc17,relation_dom(skc14))* equal(apply(skc14,skc18),skc19). % 48.79/48.98 599[4:Spt:598.1] || -> equal(apply(skc14,skc18),skc19)**. % 48.79/48.98 845[0:EqR:83.2] relation(u) || in(v,relation_dom(u)) -> in(ordered_pair(v,skf15(u,v)),u)*. % 48.79/48.98 965[0:Res:95.4,79.2] function(u) relation(u) relation(u) || in(v,relation_dom(u))* equal(w,apply(u,v))* equal(x,relation_rng(u))* -> in(w,x)*. % 48.79/48.98 980[0:Obv:965.1] function(u) relation(u) || in(v,relation_dom(u))* equal(w,apply(u,v))*+ equal(x,relation_rng(u))* -> in(w,x)*. % 48.79/48.98 1185[0:Res:99.3,78.2] relation(u) relation(v) relation(v) || equal(w,relation_dom(v)) -> equal(u,relation_inverse(v)) in(ordered_pair(skf24(v,u),skf23(v,u)),u)* in(skf23(v,u),w)*. % 48.79/48.98 1187[0:Res:99.3,94.3] relation(u) relation(v) function(v) relation(v) || in(skf23(v,u),relation_dom(v)) -> equal(u,relation_inverse(v)) in(ordered_pair(skf24(v,u),skf23(v,u)),u)* equal(apply(v,skf23(v,u)),skf24(v,u)). % 48.79/48.98 1197[0:Res:99.4,78.2] relation(u) relation(v) relation(u) || equal(w,relation_dom(u)) -> equal(u,relation_inverse(v)) in(ordered_pair(skf23(v,u),skf24(v,u)),v)* in(skf24(v,u),w)*. % 48.79/48.98 1199[0:Res:99.4,94.3] relation(u) relation(v) function(u) relation(u) || in(skf24(v,u),relation_dom(u)) -> equal(u,relation_inverse(v)) in(ordered_pair(skf23(v,u),skf24(v,u)),v)* equal(apply(u,skf24(v,u)),skf23(v,u)). % 48.79/48.98 1212[0:Obv:1197.0] relation(u) relation(v) || equal(w,relation_dom(v))+ -> equal(v,relation_inverse(u)) in(ordered_pair(skf23(u,v),skf24(u,v)),u)* in(skf24(u,v),w)*. % 48.79/48.98 1214[0:Obv:1185.1] relation(u) relation(v) || equal(w,relation_dom(v))+ -> equal(u,relation_inverse(v)) in(ordered_pair(skf24(v,u),skf23(v,u)),u)* in(skf23(v,u),w)*. % 48.79/48.98 1221[0:Obv:1199.0] relation(u) function(v) relation(v) || in(skf24(u,v),relation_dom(v)) -> equal(v,relation_inverse(u)) in(ordered_pair(skf23(u,v),skf24(u,v)),u)* equal(apply(v,skf24(u,v)),skf23(u,v)). % 48.79/48.98 1222[0:Obv:1187.1] relation(u) function(v) relation(v) || in(skf23(v,u),relation_dom(v)) -> equal(u,relation_inverse(v)) in(ordered_pair(skf24(v,u),skf23(v,u)),u)* equal(apply(v,skf23(v,u)),skf24(v,u)). % 48.79/48.98 2038[0:EqR:136.1] || in(u,relation_dom(skc14)) -> in(ordered_pair(u,skf15(skc14,u)),skc14)*. % 48.79/48.98 2187[0:Res:845.2,214.1] relation(skc14) || in(u,relation_dom(skc14))* in(u,relation_dom(skc14))* -> equal(skf15(skc14,u),apply(skc14,u)). % 48.79/48.98 2194[0:Obv:2187.1] relation(skc14) || in(u,relation_dom(skc14))* -> equal(skf15(skc14,u),apply(skc14,u)). % 48.79/48.98 2195[0:SSi:2194.0,4.0,3.0,2.0] || in(u,relation_dom(skc14))* -> equal(skf15(skc14,u),apply(skc14,u)). % 48.79/48.98 2197[0:Rew:2195.1,2038.1] || in(u,relation_dom(skc14)) -> in(ordered_pair(u,apply(skc14,u)),skc14)*. % 48.79/48.98 3339[3:Res:590.0,2195.0] || -> equal(skf15(skc14,skc18),apply(skc14,skc18))**. % 48.79/48.98 3346[4:Rew:599.0,3339.0] || -> equal(skf15(skc14,skc18),skc19)**. % 48.79/48.98 3368[4:SpR:3346.0,845.2] relation(skc14) || in(skc18,relation_dom(skc14)) -> in(ordered_pair(skc18,skc19),skc14)*. % 48.79/48.98 3370[4:SSi:3368.0,4.0,3.0,2.0] || in(skc18,relation_dom(skc14)) -> in(ordered_pair(skc18,skc19),skc14)*. % 48.79/48.98 3371[4:MRR:3370.0,590.0] || -> in(ordered_pair(skc18,skc19),skc14)*. % 48.79/48.98 3398[4:Res:3371.0,480.1] || equal(u,relation_dom(skc14)) -> in(skc19,u)*. % 48.79/48.98 3400[4:Res:3371.0,484.0] || -> in(ordered_pair(skc19,skc18),skc14)*. % 48.79/48.98 3424[4:Res:3400.0,214.1] || in(skc19,relation_dom(skc14))* -> equal(apply(skc14,skc19),skc18). % 48.79/48.98 3425[4:MRR:3424.1,482.1] || in(skc19,relation_dom(skc14))* -> . % 48.79/48.98 3478[4:Res:3398.1,3425.0] || equal(relation_dom(skc14),relation_dom(skc14))* -> . % 48.79/48.98 3479[4:Obv:3478.0] || -> . % 48.79/48.98 3482[4:Spt:3479.0,598.1,599.0] || equal(apply(skc14,skc18),skc19)** -> . % 48.79/48.98 3483[4:Spt:3479.0,598.0] || -> in(skc17,relation_dom(skc14))*. % 48.79/48.98 3484[4:MRR:597.1,3482.0] || -> equal(apply(skc14,skc17),skc16)**. % 48.79/48.98 3485[4:MRR:490.1,3482.0] || SkP0(skc14,skc16,skc14,skc17)* -> . % 48.79/48.98 3491[4:Res:3483.0,2195.0] || -> equal(skf15(skc14,skc17),apply(skc14,skc17))**. % 48.79/48.98 3492[4:Rew:3484.0,3491.0] || -> equal(skf15(skc14,skc17),skc16)**. % 48.79/48.98 3498[4:SpR:3492.0,845.2] relation(skc14) || in(skc17,relation_dom(skc14)) -> in(ordered_pair(skc17,skc16),skc14)*. % 48.79/48.98 3500[4:SSi:3498.0,4.0,3.0,2.0] || in(skc17,relation_dom(skc14)) -> in(ordered_pair(skc17,skc16),skc14)*. % 48.79/48.98 3501[4:MRR:3500.0,3483.0] || -> in(ordered_pair(skc17,skc16),skc14)*. % 48.79/48.98 3517[4:Res:3501.0,480.1] || equal(u,relation_dom(skc14)) -> in(skc16,u)*. % 48.79/48.98 3519[4:Res:3501.0,484.0] || -> in(ordered_pair(skc16,skc17),skc14)*. % 48.79/48.98 3543[4:Res:3519.0,214.1] || in(skc16,relation_dom(skc14))* -> equal(apply(skc14,skc16),skc17). % 48.79/48.98 3550[4:Res:77.2,3485.0] || in(skc16,relation_dom(skc14))* equal(apply(skc14,skc16),skc17) -> . % 48.79/48.98 3552[4:Rew:3543.1,3550.1] || in(skc16,relation_dom(skc14))* equal(skc17,skc17) -> . % 48.79/48.98 3553[4:Obv:3552.1] || in(skc16,relation_dom(skc14))* -> . % 48.79/48.98 3596[4:Res:3517.1,3553.0] || equal(relation_dom(skc14),relation_dom(skc14))* -> . % 48.79/48.98 3597[4:Obv:3596.0] || -> . % 48.79/48.98 3600[3:Spt:3597.0,589.1,590.0] || in(skc18,relation_dom(skc14))* -> . % 48.79/48.98 3601[3:Spt:3597.0,589.0] || -> equal(apply(skc14,skc17),skc16)**. % 48.79/48.98 3602[3:MRR:567.1,3600.0] || -> in(skc17,relation_dom(skc14))*. % 48.79/48.98 3607[3:MRR:487.1,3600.0] || SkP0(skc14,skc16,skc14,skc17)* -> . % 48.79/48.98 3647[3:Res:3602.0,2195.0] || -> equal(skf15(skc14,skc17),apply(skc14,skc17))**. % 48.79/48.98 3648[3:Rew:3601.0,3647.0] || -> equal(skf15(skc14,skc17),skc16)**. % 48.79/48.98 3662[3:Res:77.2,3607.0] || in(skc16,relation_dom(skc14))* equal(apply(skc14,skc16),skc17) -> . % 48.79/48.98 3680[3:SpR:3648.0,845.2] relation(skc14) || in(skc17,relation_dom(skc14)) -> in(ordered_pair(skc17,skc16),skc14)*. % 48.79/48.98 3682[3:SSi:3680.0,4.0,3.0,2.0] || in(skc17,relation_dom(skc14)) -> in(ordered_pair(skc17,skc16),skc14)*. % 48.79/48.98 3683[3:MRR:3682.0,3602.0] || -> in(ordered_pair(skc17,skc16),skc14)*. % 48.79/48.98 3701[3:Res:3683.0,480.1] || equal(u,relation_dom(skc14)) -> in(skc16,u)*. % 48.79/48.98 3703[3:Res:3683.0,484.0] || -> in(ordered_pair(skc16,skc17),skc14)*. % 48.79/48.98 3738[3:Res:3703.0,214.1] || in(skc16,relation_dom(skc14))* -> equal(apply(skc14,skc16),skc17). % 48.79/48.98 3739[3:MRR:3738.1,3662.1] || in(skc16,relation_dom(skc14))* -> . % 48.79/48.98 3792[3:Res:3701.1,3739.0] || equal(relation_dom(skc14),relation_dom(skc14))* -> . % 48.79/48.98 3793[3:Obv:3792.0] || -> . % 48.79/48.98 3796[2:Spt:3793.0,304.0,463.0] || equal(relation_inverse(skc14),skc14)** -> . % 48.79/48.98 3797[2:Spt:3793.0,304.1] || -> equal(relation_rng(skc14),relation_dom(skc14))**. % 48.79/48.98 3819[2:MRR:323.3,3796.0] || in(u,relation_dom(skc14))* equal(v,apply(skc14,u))*+ -> in(v,relation_dom(skc14))*. % 48.79/48.98 3820[2:MRR:328.3,3796.0] || in(u,relation_dom(skc14))* equal(v,apply(skc14,u))*+ -> equal(u,apply(skc14,v))*. % 48.79/48.98 3825[2:MRR:331.0,3796.0] || -> in(ordered_pair(skf23(skc14,skc14),skf24(skc14,skc14)),skc14) in(ordered_pair(skf24(skc14,skc14),skf23(skc14,skc14)),skc14)*. % 48.79/48.98 3826[2:MRR:334.2,3796.0] || in(ordered_pair(skf23(skc14,skc14),skf24(skc14,skc14)),skc14) in(ordered_pair(skf24(skc14,skc14),skf23(skc14,skc14)),skc14)* -> . % 48.79/48.98 3955[2:EqR:3819.1] || in(u,relation_dom(skc14)) -> in(apply(skc14,u),relation_dom(skc14))*. % 48.79/48.98 4013[2:EqR:3820.1] || in(u,relation_dom(skc14)) -> equal(apply(skc14,apply(skc14,u)),u)**. % 48.79/48.98 4063[2:SpR:4013.1,2197.1] || in(u,relation_dom(skc14)) in(apply(skc14,u),relation_dom(skc14)) -> in(ordered_pair(apply(skc14,u),u),skc14)*. % 48.79/48.98 4083[2:MRR:4063.1,3955.1] || in(u,relation_dom(skc14)) -> in(ordered_pair(apply(skc14,u),u),skc14)*. % 48.79/48.98 7038[0:EqR:1212.2] relation(u) relation(v) || -> equal(v,relation_inverse(u)) in(ordered_pair(skf23(u,v),skf24(u,v)),u)* in(skf24(u,v),relation_dom(v)). % 48.79/48.98 7044[0:MRR:1221.3,7038.4] relation(u) function(v) relation(v) || -> equal(v,relation_inverse(u)) in(ordered_pair(skf23(u,v),skf24(u,v)),u)* equal(apply(v,skf24(u,v)),skf23(u,v)). % 48.79/48.98 7230[0:EqR:1214.2] relation(u) relation(v) || -> equal(u,relation_inverse(v)) in(ordered_pair(skf24(v,u),skf23(v,u)),u)* in(skf23(v,u),relation_dom(v)). % 48.79/48.98 7236[0:MRR:1222.3,7230.4] relation(u) function(v) relation(v) || -> equal(u,relation_inverse(v)) in(ordered_pair(skf24(v,u),skf23(v,u)),u)* equal(apply(v,skf23(v,u)),skf24(v,u)). % 48.79/48.98 13114[3:Spt:3825.0] || -> in(ordered_pair(skf23(skc14,skc14),skf24(skc14,skc14)),skc14)*. % 48.79/48.98 13115[3:MRR:3826.0,13114.0] || in(ordered_pair(skf24(skc14,skc14),skf23(skc14,skc14)),skc14)* -> . % 48.79/48.98 13134[3:Res:13114.0,138.1] || equal(u,relation_dom(skc14)) -> in(skf23(skc14,skc14),u)*. % 48.79/48.98 13141[3:Res:7236.4,13115.0] relation(skc14) function(skc14) relation(skc14) || -> equal(relation_inverse(skc14),skc14) equal(apply(skc14,skf23(skc14,skc14)),skf24(skc14,skc14))**. % 48.79/48.98 13149[3:Obv:13141.0] function(skc14) relation(skc14) || -> equal(relation_inverse(skc14),skc14) equal(apply(skc14,skf23(skc14,skc14)),skf24(skc14,skc14))**. % 48.79/48.98 13150[3:SSi:13149.1,13149.0,4.0,3.0,2.0,4.0,3.0,2.0] || -> equal(relation_inverse(skc14),skc14) equal(apply(skc14,skf23(skc14,skc14)),skf24(skc14,skc14))**. % 48.79/48.98 13151[3:MRR:13150.0,3796.0] || -> equal(apply(skc14,skf23(skc14,skc14)),skf24(skc14,skc14))**. % 48.79/48.98 13156[3:SpR:13151.0,4083.1] || in(skf23(skc14,skc14),relation_dom(skc14)) -> in(ordered_pair(skf24(skc14,skc14),skf23(skc14,skc14)),skc14)*. % 48.79/48.98 13172[3:MRR:13156.1,13115.0] || in(skf23(skc14,skc14),relation_dom(skc14))* -> . % 48.79/48.98 13513[3:Res:13134.1,13172.0] || equal(relation_dom(skc14),relation_dom(skc14))* -> . % 48.79/48.98 13526[3:Obv:13513.0] || -> . % 48.79/48.98 13538[3:Spt:13526.0,3825.0,13114.0] || in(ordered_pair(skf23(skc14,skc14),skf24(skc14,skc14)),skc14)* -> . % 48.79/48.98 13539[3:Spt:13526.0,3825.1] || -> in(ordered_pair(skf24(skc14,skc14),skf23(skc14,skc14)),skc14)*. % 48.79/48.98 13556[3:Res:13539.0,138.1] || equal(u,relation_dom(skc14)) -> in(skf24(skc14,skc14),u)*. % 48.79/48.98 13566[3:Res:7044.4,13538.0] relation(skc14) function(skc14) relation(skc14) || -> equal(relation_inverse(skc14),skc14) equal(apply(skc14,skf24(skc14,skc14)),skf23(skc14,skc14))**. % 48.79/48.98 13571[3:Obv:13566.0] function(skc14) relation(skc14) || -> equal(relation_inverse(skc14),skc14) equal(apply(skc14,skf24(skc14,skc14)),skf23(skc14,skc14))**. % 48.79/48.98 13572[3:SSi:13571.1,13571.0,4.0,3.0,2.0,4.0,3.0,2.0] || -> equal(relation_inverse(skc14),skc14) equal(apply(skc14,skf24(skc14,skc14)),skf23(skc14,skc14))**. % 48.79/48.98 13573[3:MRR:13572.0,3796.0] || -> equal(apply(skc14,skf24(skc14,skc14)),skf23(skc14,skc14))**. % 48.79/48.98 13578[3:SpR:13573.0,4083.1] || in(skf24(skc14,skc14),relation_dom(skc14)) -> in(ordered_pair(skf23(skc14,skc14),skf24(skc14,skc14)),skc14)*. % 48.79/48.98 13594[3:MRR:13578.1,13538.0] || in(skf24(skc14,skc14),relation_dom(skc14))* -> . % 48.79/48.98 13921[3:Res:13556.1,13594.0] || equal(relation_dom(skc14),relation_dom(skc14))* -> . % 48.79/48.98 13934[3:Obv:13921.0] || -> . % 48.79/48.98 13946[1:Spt:13934.0,227.0,243.0] || equal(skc15,skc14)** -> . % 48.79/48.98 13947[1:Spt:13934.0,227.1,227.2] || -> in(ordered_pair(skf14(skc15,skc14),skf13(skc15,skc14)),skc15)* in(ordered_pair(skf14(skc15,skc14),skf13(skc15,skc14)),skc14). % 48.79/48.98 14072[2:Spt:203.0] || -> equal(relation_inverse(skc14),skc15)**. % 48.79/48.98 14076[2:Rew:14072.0,148.0] || -> equal(relation_inverse(skc15),skc14)**. % 48.79/48.98 14077[2:Rew:14072.0,147.0] || -> equal(relation_rng(skc15),relation_dom(skc14))**. % 48.79/48.98 14213[2:Rew:14072.0,146.0] || -> equal(relation_rng(skc14),relation_dom(skc15))**. % 48.79/48.98 14219[2:Rew:14072.0,199.0] || equal(skc15,skc15) equal(relation_rng(skc14),relation_dom(skc15)) SkP0(skc15,skc16,skc14,skc17)* -> equal(apply(skc14,skc18),skc19). % 48.79/48.98 14220[2:Rew:14072.0,200.0] || equal(skc15,skc15) equal(relation_rng(skc14),relation_dom(skc15)) SkP0(skc15,skc16,skc14,skc17)* -> in(skc18,relation_dom(skc14)). % 48.79/48.98 14221[2:Rew:14072.0,238.0] || equal(skc15,skc15) in(ordered_pair(u,v),skc15)* -> in(ordered_pair(v,u),skc14)*. % 48.79/48.98 14241[2:Rew:14076.0,163.1] relation(u) || equal(u,skc14) in(ordered_pair(v,w),u)*+ -> in(ordered_pair(w,v),skc15)*. % 48.79/48.98 14245[2:Rew:14077.0,173.0] || equal(u,relation_dom(skc14)) in(ordered_pair(v,w),skc15)*+ -> in(w,u)*. % 48.79/48.98 14307[2:Rew:14213.0,68.0] || in(skc19,relation_dom(skc15))* equal(apply(skc15,skc19),skc18) -> . % 48.79/48.98 14363[2:Obv:14221.0] || in(ordered_pair(u,v),skc15)*+ -> in(ordered_pair(v,u),skc14)*. % 48.79/48.98 14368[2:Obv:14220.0] || equal(relation_rng(skc14),relation_dom(skc15)) SkP0(skc15,skc16,skc14,skc17)* -> in(skc18,relation_dom(skc14)). % 48.79/48.98 14369[2:Rew:14213.0,14368.0] || equal(relation_dom(skc15),relation_dom(skc15)) SkP0(skc15,skc16,skc14,skc17)* -> in(skc18,relation_dom(skc14)). % 48.79/48.98 14370[2:Obv:14369.0] || SkP0(skc15,skc16,skc14,skc17)* -> in(skc18,relation_dom(skc14)). % 48.79/48.98 14372[2:Obv:14219.0] || equal(relation_rng(skc14),relation_dom(skc15)) SkP0(skc15,skc16,skc14,skc17)* -> equal(apply(skc14,skc18),skc19). % 48.79/48.98 14373[2:Rew:14213.0,14372.0] || equal(relation_dom(skc15),relation_dom(skc15)) SkP0(skc15,skc16,skc14,skc17)* -> equal(apply(skc14,skc18),skc19). % 48.79/48.98 14374[2:Obv:14373.0] || SkP0(skc15,skc16,skc14,skc17)* -> equal(apply(skc14,skc18),skc19). % 48.79/48.98 14459[2:Res:57.1,14370.0] || -> in(skc17,relation_rng(skc14)) in(skc18,relation_dom(skc14))*. % 48.79/48.98 14460[2:Res:66.1,14370.0] || -> equal(apply(skc15,skc17),skc16) in(skc18,relation_dom(skc14))*. % 48.79/48.98 14461[2:Res:77.2,14370.0] || in(skc16,relation_dom(skc14)) equal(apply(skc14,skc16),skc17) -> in(skc18,relation_dom(skc14))*. % 48.79/48.98 14462[2:Rew:14213.0,14459.0] || -> in(skc17,relation_dom(skc15)) in(skc18,relation_dom(skc14))*. % 48.79/48.98 14538[2:Res:57.1,14374.0] || -> in(skc17,relation_rng(skc14))* equal(apply(skc14,skc18),skc19). % 48.79/48.98 14539[2:Res:66.1,14374.0] || -> equal(apply(skc15,skc17),skc16)** equal(apply(skc14,skc18),skc19). % 48.79/48.98 14540[2:Res:77.2,14374.0] || in(skc16,relation_dom(skc14))* equal(apply(skc14,skc16),skc17) -> equal(apply(skc14,skc18),skc19). % 48.79/48.98 14541[2:Rew:14213.0,14538.0] || -> in(skc17,relation_dom(skc15))* equal(apply(skc14,skc18),skc19). % 48.79/48.98 14551[3:Spt:14462.1] || -> in(skc18,relation_dom(skc14))*. % 48.79/48.98 14574[4:Spt:14541.1] || -> equal(apply(skc14,skc18),skc19)**. % 48.79/48.98 14576[4:SpR:14574.0,2197.1] || in(skc18,relation_dom(skc14)) -> in(ordered_pair(skc18,skc19),skc14)*. % 48.79/48.98 14586[4:MRR:14576.0,14551.0] || -> in(ordered_pair(skc18,skc19),skc14)*. % 48.79/48.98 14606[4:Res:14586.0,79.2] relation(skc14) || equal(u,relation_rng(skc14)) -> in(skc19,u)*. % 48.79/48.98 14617[4:Rew:14213.0,14606.1] relation(skc14) || equal(u,relation_dom(skc15)) -> in(skc19,u)*. % 48.79/48.98 14618[4:SSi:14617.0,4.0,3.0,2.0] || equal(u,relation_dom(skc15)) -> in(skc19,u)*. % 48.79/48.98 14773[4:Res:14618.1,14307.0] || equal(relation_dom(skc15),relation_dom(skc15)) equal(apply(skc15,skc19),skc18)** -> . % 48.79/48.98 14785[4:Obv:14773.0] || equal(apply(skc15,skc19),skc18)** -> . % 48.79/48.98 15056[0:Res:845.2,212.1] relation(skc15) || in(u,relation_dom(skc15))* in(u,relation_dom(skc15))* -> equal(skf15(skc15,u),apply(skc15,u)). % 48.79/48.98 15079[0:Obv:15056.1] relation(skc15) || in(u,relation_dom(skc15))* -> equal(skf15(skc15,u),apply(skc15,u)). % 48.79/48.98 15080[0:SSi:15079.0,1.0,5.0] || in(u,relation_dom(skc15))* -> equal(skf15(skc15,u),apply(skc15,u)). % 48.79/48.98 16011[4:Res:14586.0,14241.2] relation(skc14) || equal(skc14,skc14) -> in(ordered_pair(skc19,skc18),skc15)*. % 48.79/48.98 16030[4:Obv:16011.1] relation(skc14) || -> in(ordered_pair(skc19,skc18),skc15)*. % 48.79/48.98 16031[4:SSi:16030.0,4.0,3.0,2.0] || -> in(ordered_pair(skc19,skc18),skc15)*. % 48.79/48.98 16100[4:Res:16031.0,212.1] || in(skc19,relation_dom(skc15))* -> equal(apply(skc15,skc19),skc18). % 48.79/48.98 16101[4:MRR:16100.1,14785.0] || in(skc19,relation_dom(skc15))* -> . % 48.79/48.98 16109[4:Res:14618.1,16101.0] || equal(relation_dom(skc15),relation_dom(skc15))* -> . % 48.79/48.98 16118[4:Obv:16109.0] || -> . % 48.79/48.98 16119[4:Spt:16118.0,14541.1,14574.0] || equal(apply(skc14,skc18),skc19)** -> . % 48.79/48.98 16120[4:Spt:16118.0,14541.0] || -> in(skc17,relation_dom(skc15))*. % 48.79/48.98 16121[4:MRR:14539.1,16119.0] || -> equal(apply(skc15,skc17),skc16)**. % 48.79/48.98 16124[4:MRR:14540.2,16119.0] || in(skc16,relation_dom(skc14))* equal(apply(skc14,skc16),skc17) -> . % 48.79/48.98 18315[4:Res:16120.0,15080.0] || -> equal(skf15(skc15,skc17),apply(skc15,skc17))**. % 48.79/48.98 18341[4:Rew:16121.0,18315.0] || -> equal(skf15(skc15,skc17),skc16)**. % 48.79/48.98 18382[4:SpR:18341.0,845.2] relation(skc15) || in(skc17,relation_dom(skc15)) -> in(ordered_pair(skc17,skc16),skc15)*. % 48.79/48.98 18385[4:SSi:18382.0,1.0,5.0] || in(skc17,relation_dom(skc15)) -> in(ordered_pair(skc17,skc16),skc15)*. % 48.82/48.98 18386[4:MRR:18385.0,16120.0] || -> in(ordered_pair(skc17,skc16),skc15)*. % 48.82/48.98 18407[4:Res:18386.0,14245.1] || equal(u,relation_dom(skc14)) -> in(skc16,u)*. % 48.82/48.98 18409[4:Res:18386.0,14363.0] || -> in(ordered_pair(skc16,skc17),skc14)*. % 48.82/48.98 18437[4:Res:18409.0,214.1] || in(skc16,relation_dom(skc14))* -> equal(apply(skc14,skc16),skc17). % 48.82/48.98 18438[4:MRR:18437.1,16124.1] || in(skc16,relation_dom(skc14))* -> . % 48.82/48.98 18551[4:Res:18407.1,18438.0] || equal(relation_dom(skc14),relation_dom(skc14))* -> . % 48.82/48.98 18565[4:Obv:18551.0] || -> . % 48.82/48.98 18569[3:Spt:18565.0,14462.1,14551.0] || in(skc18,relation_dom(skc14))* -> . % 48.82/48.98 18570[3:Spt:18565.0,14462.0] || -> in(skc17,relation_dom(skc15))*. % 48.82/48.98 18571[3:MRR:14460.1,18569.0] || -> equal(apply(skc15,skc17),skc16)**. % 48.82/48.98 18574[3:MRR:14461.2,18569.0] || in(skc16,relation_dom(skc14))* equal(apply(skc14,skc16),skc17) -> . % 48.82/48.98 18608[3:Res:18570.0,15080.0] || -> equal(skf15(skc15,skc17),apply(skc15,skc17))**. % 48.82/48.98 18609[3:Rew:18571.0,18608.0] || -> equal(skf15(skc15,skc17),skc16)**. % 48.82/48.98 18620[3:SpL:18571.0,980.3] function(skc15) relation(skc15) || in(skc17,relation_dom(skc15))* equal(u,skc16) equal(v,relation_rng(skc15)) -> in(u,v)*. % 48.82/48.98 18624[3:Rew:14077.0,18620.4] function(skc15) relation(skc15) || in(skc17,relation_dom(skc15))* equal(u,skc16) equal(v,relation_dom(skc14)) -> in(u,v)*. % 48.82/48.98 18625[3:SSi:18624.1,18624.0,1.0,5.0,1.0,5.0] || in(skc17,relation_dom(skc15))* equal(u,skc16) equal(v,relation_dom(skc14)) -> in(u,v)*. % 48.82/48.98 18626[3:MRR:18625.0,18570.0] || equal(u,skc16) equal(v,relation_dom(skc14)) -> in(u,v)*. % 48.82/48.98 18636[3:SpR:18609.0,845.2] relation(skc15) || in(skc17,relation_dom(skc15)) -> in(ordered_pair(skc17,skc16),skc15)*. % 48.82/48.98 18639[3:SSi:18636.0,1.0,5.0] || in(skc17,relation_dom(skc15)) -> in(ordered_pair(skc17,skc16),skc15)*. % 48.82/48.98 18640[3:MRR:18639.0,18570.0] || -> in(ordered_pair(skc17,skc16),skc15)*. % 48.82/48.98 18677[3:Res:18640.0,14363.0] || -> in(ordered_pair(skc16,skc17),skc14)*. % 48.82/48.98 18705[3:Res:18677.0,214.1] || in(skc16,relation_dom(skc14))* -> equal(apply(skc14,skc16),skc17). % 48.82/48.98 18706[3:MRR:18705.1,18574.1] || in(skc16,relation_dom(skc14))* -> . % 48.82/48.98 18799[3:Res:18626.2,18706.0] || equal(skc16,skc16) equal(relation_dom(skc14),relation_dom(skc14))* -> . % 48.82/48.98 18857[3:Obv:18799.1] || -> . % 48.82/48.98 18866[2:Spt:18857.0,203.0,14072.0] || equal(relation_inverse(skc14),skc15)** -> . % 48.82/48.98 18867[2:Spt:18857.0,203.1] || -> equal(relation_rng(skc14),relation_dom(skc15))**. % 48.82/48.98 18879[2:MRR:204.0,18866.0] || -> SkP0(skc15,u,skc14,v)*. % 48.82/48.98 18891[2:Rew:18867.0,139.0] || equal(u,relation_dom(skc15)) in(ordered_pair(v,w),skc14)*+ -> in(w,u)*. % 48.82/48.98 18952[2:MRR:201.3,18866.0] || in(u,relation_dom(skc14))* equal(v,apply(skc14,u))*+ -> equal(u,apply(skc15,v))*. % 48.82/48.98 18966[2:MRR:223.0,18866.0] || -> in(ordered_pair(skf23(skc14,skc15),skf24(skc14,skc15)),skc14) in(ordered_pair(skf24(skc14,skc15),skf23(skc14,skc15)),skc15)*. % 48.82/48.98 18990[2:MRR:215.2,18866.0] || in(ordered_pair(skf23(skc14,skc15),skf24(skc14,skc15)),skc14) in(ordered_pair(skf24(skc14,skc15),skf23(skc14,skc15)),skc15)* -> . % 48.82/48.98 19193[2:Res:18879.0,96.2] || in(u,relation_rng(skc14))* equal(v,apply(skc15,u))* -> equal(u,apply(skc14,v))*. % 48.82/48.98 19194[2:Res:18879.0,90.2] || in(u,relation_rng(skc14))* equal(v,apply(skc15,u))* -> in(v,relation_dom(skc14))*. % 48.82/48.98 19195[2:Rew:18867.0,19194.0] || in(u,relation_dom(skc15))* equal(v,apply(skc15,u))*+ -> in(v,relation_dom(skc14))*. % 48.82/48.98 19196[2:Rew:18867.0,19193.0] || in(u,relation_dom(skc15))* equal(v,apply(skc15,u))*+ -> equal(u,apply(skc14,v))*. % 48.82/48.98 19349[2:EqR:18952.1] || in(u,relation_dom(skc14)) -> equal(apply(skc15,apply(skc14,u)),u)**. % 48.82/48.98 20087[2:EqR:19195.1] || in(u,relation_dom(skc15)) -> in(apply(skc15,u),relation_dom(skc14))*. % 48.82/48.98 20522[2:EqR:19196.1] || in(u,relation_dom(skc15)) -> equal(apply(skc14,apply(skc15,u)),u)**. % 48.82/48.98 21829[0:Res:211.2,123.1] relation(skc15) || in(skf24(skc14,skc15),relation_dom(skc15)) equal(apply(skc15,skf24(skc14,skc15)),skf23(skc14,skc15)) in(ordered_pair(skf23(skc14,skc15),skf24(skc14,skc15)),skc14)* -> equal(relation_inverse(skc14),skc15). % 48.82/48.98 21833[0:SSi:21829.0,1.0,5.0] || in(skf24(skc14,skc15),relation_dom(skc15)) equal(apply(skc15,skf24(skc14,skc15)),skf23(skc14,skc15)) in(ordered_pair(skf23(skc14,skc15),skf24(skc14,skc15)),skc14)* -> equal(relation_inverse(skc14),skc15). % 49.60/49.80 21834[2:MRR:21833.3,18866.0] || in(skf24(skc14,skc15),relation_dom(skc15)) equal(apply(skc15,skf24(skc14,skc15)),skf23(skc14,skc15)) in(ordered_pair(skf23(skc14,skc15),skf24(skc14,skc15)),skc14)* -> . % 49.60/49.80 22240[2:SpR:20522.1,2197.1] || in(u,relation_dom(skc15)) in(apply(skc15,u),relation_dom(skc14)) -> in(ordered_pair(apply(skc15,u),u),skc14)*. % 49.60/49.80 22265[2:MRR:22240.1,20087.1] || in(u,relation_dom(skc15)) -> in(ordered_pair(apply(skc15,u),u),skc14)*. % 49.60/49.80 25643[3:Spt:18966.0] || -> in(ordered_pair(skf23(skc14,skc15),skf24(skc14,skc15)),skc14)*. % 49.60/49.80 25644[3:MRR:18990.0,25643.0] || in(ordered_pair(skf24(skc14,skc15),skf23(skc14,skc15)),skc15)* -> . % 49.60/49.80 25645[3:MRR:21834.2,25643.0] || in(skf24(skc14,skc15),relation_dom(skc15))* equal(apply(skc15,skf24(skc14,skc15)),skf23(skc14,skc15)) -> . % 49.60/49.80 25664[3:Res:25643.0,18891.1] || equal(u,relation_dom(skc15)) -> in(skf24(skc14,skc15),u)*. % 49.60/49.80 25667[3:Res:25643.0,138.1] || equal(u,relation_dom(skc14)) -> in(skf23(skc14,skc15),u)*. % 49.60/49.80 25674[3:Res:7236.4,25644.0] relation(skc15) function(skc14) relation(skc14) || -> equal(relation_inverse(skc14),skc15) equal(apply(skc14,skf23(skc14,skc15)),skf24(skc14,skc15))**. % 49.60/49.80 25682[3:SSi:25674.2,25674.1,25674.0,4.0,3.0,2.0,4.0,3.0,2.0,1.0,5.0] || -> equal(relation_inverse(skc14),skc15) equal(apply(skc14,skf23(skc14,skc15)),skf24(skc14,skc15))**. % 49.60/49.80 25683[3:MRR:25682.0,18866.0] || -> equal(apply(skc14,skf23(skc14,skc15)),skf24(skc14,skc15))**. % 49.60/49.80 25686[3:SpR:25683.0,19349.1] || in(skf23(skc14,skc15),relation_dom(skc14))* -> equal(apply(skc15,skf24(skc14,skc15)),skf23(skc14,skc15)). % 49.60/49.80 25796[3:Res:25664.1,25645.0] || equal(relation_dom(skc15),relation_dom(skc15)) equal(apply(skc15,skf24(skc14,skc15)),skf23(skc14,skc15))** -> . % 49.60/49.80 25800[3:Obv:25796.0] || equal(apply(skc15,skf24(skc14,skc15)),skf23(skc14,skc15))** -> . % 49.60/49.80 25801[3:MRR:25686.1,25800.0] || in(skf23(skc14,skc15),relation_dom(skc14))* -> . % 49.60/49.80 26257[3:Res:25667.1,25801.0] || equal(relation_dom(skc14),relation_dom(skc14))* -> . % 49.60/49.80 26272[3:Obv:26257.0] || -> . % 49.60/49.80 26280[3:Spt:26272.0,18966.0,25643.0] || in(ordered_pair(skf23(skc14,skc15),skf24(skc14,skc15)),skc14)* -> . % 49.60/49.80 26281[3:Spt:26272.0,18966.1] || -> in(ordered_pair(skf24(skc14,skc15),skf23(skc14,skc15)),skc15)*. % 49.60/49.80 26308[3:Res:26281.0,172.1] || equal(u,relation_dom(skc15)) -> in(skf24(skc14,skc15),u)*. % 49.60/49.80 26344[3:Res:7044.4,26280.0] relation(skc14) function(skc15) relation(skc15) || -> equal(relation_inverse(skc14),skc15) equal(apply(skc15,skf24(skc14,skc15)),skf23(skc14,skc15))**. % 49.60/49.80 26348[3:SSi:26344.2,26344.1,26344.0,1.0,5.0,1.0,5.0,4.0,3.0,2.0] || -> equal(relation_inverse(skc14),skc15) equal(apply(skc15,skf24(skc14,skc15)),skf23(skc14,skc15))**. % 49.60/49.80 26349[3:MRR:26348.0,18866.0] || -> equal(apply(skc15,skf24(skc14,skc15)),skf23(skc14,skc15))**. % 49.60/49.80 28614[3:SpR:26349.0,22265.1] || in(skf24(skc14,skc15),relation_dom(skc15)) -> in(ordered_pair(skf23(skc14,skc15),skf24(skc14,skc15)),skc14)*. % 49.60/49.80 28639[3:MRR:28614.1,26280.0] || in(skf24(skc14,skc15),relation_dom(skc15))* -> . % 49.60/49.80 28647[3:Res:26308.1,28639.0] || equal(relation_dom(skc15),relation_dom(skc15))* -> . % 49.60/49.80 28651[3:Obv:28647.0] || -> . % 49.60/49.80 % SZS output end Refutation % 49.60/49.80 Formulae used in the proof : t54_funct_1 antisymmetry_r2_hidden involutiveness_k4_relat_1 t37_relat_1 d9_funct_1 d4_relat_1 d5_relat_1 d7_relat_1 d4_funct_1 d2_relat_1 % 49.60/49.80 %------------------------------------------------------------------------------