The mouse eats the rabbit. The mouse eats the tiger. The mouse is green. The mouse visits the rabbit. The mouse visits the tiger. The rabbit eats the tiger. The tiger eats the rabbit. The tiger is nice. The tiger is red. The tiger visits the rabbit. If someone visits the tiger and they are red then the tiger is green. If the tiger needs the mouse then the mouse does not eat the tiger. If the tiger needs the mouse then the mouse visits the tiger. If the tiger eats the rabbit and the tiger is not round then the rabbit eats the tiger. If someone is green then they visit the mouse. If someone is green then they are red. If someone needs the tiger and the tiger visits the rabbit then the rabbit visits the mouse. If someone needs the rabbit and they need the tiger then the rabbit needs the tiger.
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If someone visits the tiger and they are red then the tiger is green.
((("someone" "visits" "tiger" "+") ("someone" "is" "red" "+")) -> ("tiger" "is" "green" "+"))
If the tiger needs the mouse then the mouse does not eat the tiger.
((("tiger" "needs" "mouse" "+")) -> ("mouse" "eats" "tiger" "-"))
If the tiger needs the mouse then the mouse visits the tiger.
((("tiger" "needs" "mouse" "+")) -> ("mouse" "visits" "tiger" "+"))
If the tiger eats the rabbit and the tiger is not round then the rabbit eats the tiger.
((("tiger" "eats" "rabbit" "+") ("tiger" "is" "round" "~")) -> ("rabbit" "eats" "tiger" "+"))
If someone is green then they visit the mouse.
((("someone" "is" "green" "+")) -> ("someone" "visits" "mouse" "+"))
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If someone needs the tiger and the tiger visits the rabbit then the rabbit visits the mouse.
((("someone" "needs" "tiger" "+") ("tiger" "visits" "rabbit" "+")) -> ("rabbit" "visits" "mouse" "+"))
If someone needs the rabbit and they need the tiger then the rabbit needs the tiger.
((("someone" "needs" "rabbit" "+") ("someone" "needs" "tiger" "+")) -> ("rabbit" "needs" "tiger" "+"))
The tiger visits the rabbit.
True
1
proof
[(triple10)]
("tiger" "visits" "rabbit" "+")
triple10
The tiger does not visit the rabbit.
False
1
inv-proof
[(triple10)]
("tiger" "visits" "rabbit" "-")
triple10
The mouse visits the mouse.
True
2
proof
[(((triple3) -> rule5))]
("mouse" "visits" "mouse" "+")
((triple3) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is not red.
False
2
inv-proof
[(((triple3) -> rule6))]
("mouse" "is" "red" "-")
((triple3) -> (rule6 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger is green.
True
4
proof
[(((triple5 ((triple3) -> rule6)) -> rule1))]
("tiger" "is" "green" "+")
((triple5 ((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The tiger is not green.
False
4
inv-proof
[(((triple5 ((triple3) -> rule6)) -> rule1))]
("tiger" "is" "green" "-")
((triple5 ((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The tiger visits the mouse.
True
5
proof
[(((((triple5 ((triple3) -> rule6)) -> rule1)) -> rule5))]
("tiger" "visits" "mouse" "+")
((((triple5 ((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The tiger does not visit the mouse.
False
5
inv-proof
[(((((triple5 ((triple3) -> rule6)) -> rule1)) -> rule5))]
("tiger" "visits" "mouse" "-")
((((triple5 ((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "red" "-")
The rabbit visits the mouse.
Unknown
rconc
[@2: The rabbit visits the mouse.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("rabbit" "visits" "mouse" "+")
The rabbit does not need the tiger.
Unknown
inv-rconc
[@1: The rabbit needs the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "needs" "tiger" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
The mouse does not need the tiger.
Unknown
inv-random
[@0: The mouse needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "tiger" "-")
The rabbit needs the mouse.
Unknown
random
[@0: The rabbit needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "mouse" "+")
@0: The mouse eats the rabbit.[(triple1)] The mouse eats the tiger.[(triple2)] The mouse is green.[(triple3)] The mouse visits the rabbit.[(triple4)] The mouse visits the tiger.[(triple5)] The rabbit eats the tiger.[(triple6)] The tiger eats the rabbit.[(triple7)] The tiger is nice.[(triple8)] The tiger is red.[(triple9 OR ((((triple5 ((triple3) -> rule6)) -> rule1)) -> rule6))] The tiger visits the rabbit.[(triple10)] @1: The mouse is red.[(((triple3) -> rule6))] The mouse visits the mouse.[(((triple3) -> rule5))] @2: The tiger is green.[(((triple5 ((triple3) -> rule6)) -> rule1))] @3: The tiger visits the mouse.[(((((triple5 ((triple3) -> rule6)) -> rule1)) -> rule5))]
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple4
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple5
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple6
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple7
The tiger is nice.
("tiger" "is" "nice" "+")
triple8
The tiger is red.
("tiger" "is" "red" "+")
triple9
((((triple5 ((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple10
The mouse is red.
("mouse" "is" "red" "+")
((triple3) -> (rule6 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple3) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
((triple5 ((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
((((triple5 ((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3