Skip to content
Permalink
Browse files

results for codi_down_theoremsXX added

  • Loading branch information...
thahmann committed Nov 9, 2018
1 parent 8a7b711 commit 2c0cf54fc44d28a89fbaa0e76a39384471fd34c6

Large diffs are not rendered by default.

Oops, something went wrong.

Large diffs are not rendered by default.

Oops, something went wrong.
@@ -0,0 +1,141 @@
Paradox, version 3.0, 2008-07-29.
+++ PROBLEM: C:\Users\torsten\Documents\github\colore\ontologies\multidim_mereotopology_codi\theorems\conversions\codi_down_theoremsep-e1.all.tptp
Reading 'C:\Users\torsten\Documents\github\colore\ontologies\multidim_mereotopology_codi\theorems\conversions\codi_down_theoremsep-e1.all.tptp' ... OK
+++ SOLVING: C:\Users\torsten\Documents\github\colore\ontologies\multidim_mereotopology_codi\theorems\conversions\codi_down_theoremsep-e1.all.tptp
domain size 1
domain size 2
+++ BEGIN MODEL
SZS output start FiniteModel for C:\Users\torsten\Documents\github\colore\ontologies\multidim_mereotopology_codi\theorems\conversions\codi_down_theoremsep-e1.all.tptp
% domain size is 2
fof(domain, fi_domain,
(![X] : (X = "1" | X = "2"))
).

fof(c, fi_predicates,
( c("1","1") <=> $false
& c("1","2") <=> $false
& c("2","1") <=> $false
& c("2","2") <=> $true
)
).

fof(cont, fi_predicates,
( cont("1","1") <=> $false
& cont("1","2") <=> $false
& cont("2","1") <=> $false
& cont("2","2") <=> $true
)
).

fof(covers, fi_predicates,
( covers("1","1") <=> $false
& covers("1","2") <=> $false
& covers("2","1") <=> $true
& covers("2","2") <=> $false
)
).

fof(difference, fi_functors,
( difference("1","1") = "1"
& difference("1","2") = "1"
& difference("2","1") = "2"
& difference("2","2") = "1"
)
).

fof(eqdim, fi_predicates,
( eqdim("1","1") <=> $true
& eqdim("1","2") <=> $false
& eqdim("2","1") <=> $false
& eqdim("2","2") <=> $true
)
).

fof(geq, fi_predicates,
( geq("1","1") <=> $true
& geq("1","2") <=> $false
& geq("2","1") <=> $true
& geq("2","2") <=> $true
)
).

fof(gt, fi_predicates,
( gt("1","1") <=> $false
& gt("1","2") <=> $false
& gt("2","1") <=> $true
& gt("2","2") <=> $false
)
).

fof(intersection, fi_functors,
( intersection("1","1") = "1"
& intersection("1","2") = "1"
& intersection("2","1") = "1"
& intersection("2","2") = "2"
)
).

fof(leq, fi_predicates,
( leq("1","1") <=> $true
& leq("1","2") <=> $true
& leq("2","1") <=> $false
& leq("2","2") <=> $true
)
).

fof(lt, fi_predicates,
( lt("1","1") <=> $false
& lt("1","2") <=> $true
& lt("2","1") <=> $false
& lt("2","2") <=> $false
)
).

fof(maxdim, fi_predicates,
( maxdim("1") <=> $false
& maxdim("2") <=> $true
)
).

fof(mindim, fi_predicates,
( mindim("1") <=> $false
& mindim("2") <=> $true
)
).

fof(p, fi_predicates,
( p("1","1") <=> $false
& p("1","2") <=> $false
& p("2","1") <=> $false
& p("2","2") <=> $true
)
).

fof(po, fi_predicates,
( po("1","1") <=> $false
& po("1","2") <=> $false
& po("2","1") <=> $false
& po("2","2") <=> $true
)
).

fof(pp, fi_predicates,
( ![X1,X2] : pp(X1,X2) <=> $false
)
).

fof(zex, fi_predicates,
( zex("1") <=> $true
& zex("2") <=> $false
)
).
SZS output end FiniteModel for C:\Users\torsten\Documents\github\colore\ontologies\multidim_mereotopology_codi\theorems\conversions\codi_down_theoremsep-e1.all.tptp
+++ END MODEL
+++ RESULT: Satisfiable
SZS status Satisfiable for C:\Users\torsten\Documents\github\colore\ontologies\multidim_mereotopology_codi\theorems\conversions\codi_down_theoremsep-e1.all.tptp
============================= C:\Reasoning\paradox3 ================================
execution finished: Tue Apr 24 09:42:37 2018
total CPU time used: 0
The command was "C:\Reasoning\paradox3 --time 600 --verbose 2 --model --tstp C:\Users\torsten\Documents\github\colore\ontologies\multidim_mereotopology_codi\theorems\conversions\codi_down_theoremsep-e1.all.tptp"
Input read from
============================ end of footer ===========================
@@ -0,0 +1,93 @@
Hi Geoff, go and have some cold beer while I am trying to solve this very hard problem!
% remaining time: 5999 next slice time: 3
dis-4_5_bd=off:bs=off:ep=RST:fde=none:lcm=predicate:n=on:nicw=on:nwc=2:ptb=off:sio=off:spl=backtracking:ss=included:ssec=off:st=5:updr=off_3 on C:\Users\torsten\Documents\github\colore\ontologies\multidim_mereotopology_codi\theorems\conversions\codi_down_theoremsep-e1.all
Time limit reached!
------------------------------
Version: Vampire 0.6 (revision 903)
Termination reason: Time limit

Active clauses: 673
Passive clauses: 4515
Generated clauses: 7969
Final active clauses: 597
Final passive clauses: 3365
Input formulas: 39
Initial clauses: 67

Selected by SInE selection: 39
SInE iterations: 1

Duplicate literals: 28
Fw subsumption resolutions: 215

Simple tautologies: 39
Forward subsumptions: 3227

Binary resolution: 7254
Factoring: 52

Backtracking splits: 79
Backtracking splits refuted: 37

Memory used: 1791KB
Time elapsed: 0.404 s
------------------------------
% remaining time: 5995 next slice time: 13
dis-1010_2_bs=off:ep=on:n=on:nwc=1.5:sgo=on:sp=occurrence:ss=included:sswn=on:sswsr=on:st=1.5_13 on C:\Users\torsten\Documents\github\colore\ontologies\multidim_mereotopology_codi\theorems\conversions\codi_down_theoremsep-e1.all
Time limit reached!
------------------------------
Version: Vampire 0.6 (revision 903)
Termination reason: Time limit

Active clauses: 995
Passive clauses: 8156
Generated clauses: 16859
Final active clauses: 995
Final passive clauses: 6921
Input formulas: 39
Initial clauses: 62

Unused predicate definitions: 2
Selected by SInE selection: 39
SInE iterations: 1

Duplicate literals: 245
Fw subsumption resolutions: 1717

Simple tautologies: 498
Equational tautologies: 8
Forward subsumptions: 6481

Binary resolution: 10635
Factoring: 97
Forward superposition: 3534
Backward superposition: 613

Memory used: 3965KB
Time elapsed: 1.402 s
------------------------------
% remaining time: 5981 next slice time: 32
lrs+11_14_bd=off:bs=off:bsr=on:cond=on:drc=off:fde=none:fsr=off:gsp=input_only:lcm=reverse:n=on:nwc=10:ptb=off:sfv=off:sgo=on:sio=off:sos=on:sp=reverse_arity:spl=backtracking:ssec=off:stl=81_32 on C:\Users\torsten\Documents\github\colore\ontologies\multidim_mereotopology_codi\theorems\conversions\codi_down_theoremsep-e1.all
Refutation not found with incomplete strategy!
------------------------------
Version: Vampire 0.6 (revision 903)
Termination reason: Refutation not found, incomplete strategy

Active clauses: 60
Final active clauses: 60
Input formulas: 39
Initial clauses: 60

Unused predicate definitions: 2

Memory used: 127KB
Time elapsed: 0.007 s
------------------------------
% remaining time: 5981 next slice time: 95
dis+2_4_bs=off:ep=on:n=on:nicw=on:nwc=1.5:ptb=off:sac=on:sio=off:spl=backtracking:ssec=off_95 on C:\Users\torsten\Documents\github\colore\ontologies\multidim_mereotopology_codi\theorems\conversions\codi_down_theoremsep-e1.all
============================= C:\Reasoning\vampire_win ================================
execution finished: Tue Apr 24 09:42:39 2018
total CPU time used: 0
The command was "C:\Reasoning\vampire_win --mode casc --proof tptp -t 600 --input_file C:\Users\torsten\Documents\github\colore\ontologies\multidim_mereotopology_codi\theorems\conversions\codi_down_theoremsep-e1.all.tptp"
Input read from
============================ end of footer ===========================
Oops, something went wrong.

0 comments on commit 2c0cf54

Please sign in to comment.
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.