The dog is cold. The dog needs the mouse. The dog needs the rabbit. The dog sees the rabbit. The mouse eats the dog. The mouse eats the rabbit. The mouse sees the dog. The mouse sees the rabbit. The rabbit is cold. The rabbit is kind. The rabbit is nice. The rabbit needs the dog. The rabbit needs the mouse. The rabbit sees the dog. The rabbit sees the mouse. If someone sees the dog then the dog eats the mouse. If the mouse eats the dog and the dog eats the mouse then the dog eats the rabbit.
The dog is cold.
("dog" "is" "cold" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If someone sees the dog then the dog eats the mouse.
((("someone" "sees" "dog" "+")) -> ("dog" "eats" "mouse" "+"))
If the mouse eats the dog and the dog eats the mouse then the dog eats the rabbit.
((("mouse" "eats" "dog" "+") ("dog" "eats" "mouse" "+")) -> ("dog" "eats" "rabbit" "+"))
The rabbit sees the mouse.
True
1
proof
[(triple15)]
("rabbit" "sees" "mouse" "+")
triple15
The mouse does not see the dog.
False
1
inv-proof
[(triple7)]
("mouse" "sees" "dog" "-")
triple7
The dog eats the mouse.
True
2
proof
[(((triple14) -> rule1) OR ((triple7) -> rule1))]
("dog" "eats" "mouse" "+")
((triple14) -> (rule1 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
((triple7) -> (rule1 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog does not eat the mouse.
False
2
inv-proof
[(((triple14) -> rule1) OR ((triple7) -> rule1))]
("dog" "eats" "mouse" "-")
((triple14) -> (rule1 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
((triple7) -> (rule1 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog eats the rabbit.
True
4
proof
[(((triple5 ((triple14) -> rule1)) -> rule2) OR ((triple5 ((triple7) -> rule1)) -> rule2))]
("dog" "eats" "rabbit" "+")
((triple5 ((triple14) -> (rule1 % int2))) -> (rule2 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
((triple5 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The dog does not eat the rabbit.
False
4
inv-proof
[(((triple5 ((triple14) -> rule1)) -> rule2) OR ((triple5 ((triple7) -> rule1)) -> rule2))]
("dog" "eats" "rabbit" "-")
((triple5 ((triple14) -> (rule1 % int2))) -> (rule2 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
((triple5 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The mouse does not need the dog.
Unknown
inv-random
[@0: The mouse needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "dog" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The dog is cold.[(triple1)] The dog needs the mouse.[(triple2)] The dog needs the rabbit.[(triple3)] The dog sees the rabbit.[(triple4)] The mouse eats the dog.[(triple5)] The mouse eats the rabbit.[(triple6)] The mouse sees the dog.[(triple7)] The mouse sees the rabbit.[(triple8)] The rabbit is cold.[(triple9)] The rabbit is kind.[(triple10)] The rabbit is nice.[(triple11)] The rabbit needs the dog.[(triple12)] The rabbit needs the mouse.[(triple13)] The rabbit sees the dog.[(triple14)] The rabbit sees the mouse.[(triple15)] @1: The dog eats the mouse.[(((triple14) -> rule1) OR ((triple7) -> rule1))] @2: The dog eats the rabbit.[(((triple5 ((triple14) -> rule1)) -> rule2) OR ((triple5 ((triple7) -> rule1)) -> rule2))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple4
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple5
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple6
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple7
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple8
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple9
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple10
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple11
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple12
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple13
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple14
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple15
The dog eats the mouse.
("dog" "eats" "mouse" "+")
((triple14) -> (rule1 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
((triple7) -> (rule1 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
((triple5 ((triple14) -> (rule1 % int2))) -> (rule2 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
((triple5 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2