Skip to content
Permalink
Browse files

added nebesky models & input files

  • Loading branch information...
carmenchui committed Nov 10, 2018
1 parent 2c0cf54 commit 3856a1c76784a86d6cde9e97a3f24dc5f3fac915
@@ -0,0 +1,36 @@
% Saved by Prover9-Mace4 Version 0.5B, March 2008 (Dec 2007 LADR).

set(ignore_option_dependencies). % GUI handles dependencies

if(Prover9). % Options for Prover9
assign(max_seconds, 600).
end_if.

if(Mace4). % Options for Mace4
assign(max_seconds, 60).
end_if.

formulas(assumptions).

(all u all v all w (S(u,v,w) -> S(v,u,u))). %1
(all u all v all w (S(u,v,w) -> ((u != w) & (u != v)))). %2
(all u all v all w all x (S(u,v,v) & S(v,w,x) & (u != w) & -S(u,w,w) -> S(u,v,x))). %3
(all u all v all w (S(u,v,w) & (v != w) -> (exists y (S(v,y,w) & (y != u) & -S(u,y,y))))). %4
(all u all v ((u != v) -> (exists z S(u,z,v)))). %5

% reflexivity
(all x all y (S(x,y,y) <-> S(y,x,x))).

% edge definition
(all x all y (E(x,y) <-> S(x,y,y))).

% nontrivial
exists a exists b exists c exists d (E(a,b) & E(b,d) & E(c,d) & E(a,c) & E(a,d) &
a!=b & a!=c & a!=d & b!=c & b!=d & c!=d).

end_of_list.

formulas(goals).

end_of_list.

@@ -0,0 +1,176 @@
% number = 1
% seconds = 0

% Interpretation of size 4

c1 = 0.

c2 = 1.

c3 = 2.

c4 = 3.

f2(0,0) = 0.
f2(0,1) = 1.
f2(0,2) = 2.
f2(0,3) = 3.
f2(1,0) = 0.
f2(1,1) = 0.
f2(1,2) = 0.
f2(1,3) = 3.
f2(2,0) = 0.
f2(2,1) = 0.
f2(2,2) = 0.
f2(2,3) = 3.
f2(3,0) = 0.
f2(3,1) = 1.
f2(3,2) = 2.
f2(3,3) = 0.

f1(0,0,0) = 0.
f1(0,0,1) = 0.
f1(0,0,2) = 0.
f1(0,0,3) = 0.
f1(0,1,0) = 0.
f1(0,1,1) = 0.
f1(0,1,2) = 0.
f1(0,1,3) = 0.
f1(0,2,0) = 0.
f1(0,2,1) = 0.
f1(0,2,2) = 0.
f1(0,2,3) = 0.
f1(0,3,0) = 0.
f1(0,3,1) = 0.
f1(0,3,2) = 0.
f1(0,3,3) = 0.
f1(1,0,0) = 0.
f1(1,0,1) = 0.
f1(1,0,2) = 2.
f1(1,0,3) = 0.
f1(1,1,0) = 0.
f1(1,1,1) = 0.
f1(1,1,2) = 0.
f1(1,1,3) = 0.
f1(1,2,0) = 0.
f1(1,2,1) = 0.
f1(1,2,2) = 0.
f1(1,2,3) = 0.
f1(1,3,0) = 0.
f1(1,3,1) = 0.
f1(1,3,2) = 2.
f1(1,3,3) = 0.
f1(2,0,0) = 0.
f1(2,0,1) = 1.
f1(2,0,2) = 0.
f1(2,0,3) = 0.
f1(2,1,0) = 0.
f1(2,1,1) = 0.
f1(2,1,2) = 0.
f1(2,1,3) = 0.
f1(2,2,0) = 0.
f1(2,2,1) = 0.
f1(2,2,2) = 0.
f1(2,2,3) = 0.
f1(2,3,0) = 0.
f1(2,3,1) = 1.
f1(2,3,2) = 0.
f1(2,3,3) = 0.
f1(3,0,0) = 0.
f1(3,0,1) = 0.
f1(3,0,2) = 0.
f1(3,0,3) = 0.
f1(3,1,0) = 0.
f1(3,1,1) = 0.
f1(3,1,2) = 0.
f1(3,1,3) = 0.
f1(3,2,0) = 0.
f1(3,2,1) = 0.
f1(3,2,2) = 0.
f1(3,2,3) = 0.
f1(3,3,0) = 0.
f1(3,3,1) = 0.
f1(3,3,2) = 0.
f1(3,3,3) = 0.

- E(0,0).
E(0,1).
E(0,2).
E(0,3).
E(1,0).
- E(1,1).
- E(1,2).
E(1,3).
E(2,0).
- E(2,1).
- E(2,2).
E(2,3).
E(3,0).
E(3,1).
E(3,2).
- E(3,3).

- S(0,0,0).
- S(0,0,1).
- S(0,0,2).
- S(0,0,3).
- S(0,1,0).
S(0,1,1).
- S(0,1,2).
- S(0,1,3).
- S(0,2,0).
- S(0,2,1).
S(0,2,2).
- S(0,2,3).
- S(0,3,0).
- S(0,3,1).
- S(0,3,2).
S(0,3,3).
S(1,0,0).
- S(1,0,1).
S(1,0,2).
- S(1,0,3).
- S(1,1,0).
- S(1,1,1).
- S(1,1,2).
- S(1,1,3).
- S(1,2,0).
- S(1,2,1).
- S(1,2,2).
- S(1,2,3).
- S(1,3,0).
- S(1,3,1).
S(1,3,2).
S(1,3,3).
S(2,0,0).
S(2,0,1).
- S(2,0,2).
- S(2,0,3).
- S(2,1,0).
- S(2,1,1).
- S(2,1,2).
- S(2,1,3).
- S(2,2,0).
- S(2,2,1).
- S(2,2,2).
- S(2,2,3).
- S(2,3,0).
S(2,3,1).
- S(2,3,2).
S(2,3,3).
S(3,0,0).
- S(3,0,1).
- S(3,0,2).
- S(3,0,3).
- S(3,1,0).
S(3,1,1).
- S(3,1,2).
- S(3,1,3).
- S(3,2,0).
- S(3,2,1).
S(3,2,2).
- S(3,2,3).
- S(3,3,0).
- S(3,3,1).
- S(3,3,2).
- S(3,3,3).
@@ -0,0 +1,39 @@
% Saved by Prover9-Mace4 Version 0.5B, March 2008 (Dec 2007 LADR).

set(ignore_option_dependencies). % GUI handles dependencies

if(Prover9). % Options for Prover9
assign(max_seconds, 600).
end_if.

if(Mace4). % Options for Mace4
assign(start_size, 4).
assign(max_seconds, 60).
end_if.

formulas(assumptions).

(all u all v all w (S(u,v,w) -> S(v,u,u))). %1
(all u all v all w (S(u,v,w) -> ((u != w) & (u != v)))). %2
(all u all v all w all x (S(u,v,v) & S(v,w,x) & (u != w) & -S(u,w,w) -> S(u,v,x))). %3
(all u all v all w (S(u,v,w) & (v != w) -> (exists y (S(v,y,w) & (y != u) & -S(u,y,y))))). %4
(all u all v ((u != v) -> (exists z S(u,z,v)))). %5

% reflexivity
(all x all y (S(x,y,y) <-> S(y,x,x))).

% edge definition
(all x all y (E(x,y) <-> S(x,y,y))).

% nontrivial
exists a exists b exists c exists d (E(a,b) & E(b,c) & E(a,c) ).%& E(b,d)).
%exists a exists b (E(b,c) & b!=c).
%exists a exists b (E(c,d) & c!=d).
%exists a exists b (E(a,c) & a!=c).

end_of_list.

formulas(goals).

end_of_list.

Oops, something went wrong.

0 comments on commit 3856a1c

Please sign in to comment.
You can’t perform that action at this time.