The cat eats the lion. The cat eats the mouse. The cat eats the tiger. The cat is blue. The cat is red. The cat needs the mouse. The cat visits the lion. The cat visits the tiger. The lion eats the mouse. The lion is blue. The lion is cold. The mouse needs the lion. The mouse needs the tiger. The tiger eats the cat. The tiger eats the mouse. If the mouse eats the lion and the lion is cold then the mouse is big. If someone is big then they visit the mouse. If someone needs the mouse then the mouse eats the lion.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is red.
("cat" "is" "red" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
If the mouse eats the lion and the lion is cold then the mouse is big.
((("mouse" "eats" "lion" "+") ("lion" "is" "cold" "+")) -> ("mouse" "is" "big" "+"))
If someone is big then they visit the mouse.
((("someone" "is" "big" "+")) -> ("someone" "visits" "mouse" "+"))
If someone needs the mouse then the mouse eats the lion.
((("someone" "needs" "mouse" "+")) -> ("mouse" "eats" "lion" "+"))
The cat eats the lion.
True
1
proof
[(triple1)]
("cat" "eats" "lion" "+")
triple1
The lion is not cold.
False
1
inv-proof
[(triple11)]
("lion" "is" "cold" "-")
triple11
The mouse eats the lion.
True
2
proof
[(((triple6) -> rule3))]
("mouse" "eats" "lion" "+")
((triple6) -> (rule3 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse does not eat the lion.
False
2
inv-proof
[(((triple6) -> rule3))]
("mouse" "eats" "lion" "-")
((triple6) -> (rule3 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse is big.
True
4
proof
[(((((triple6) -> rule3) triple11) -> rule1))]
("mouse" "is" "big" "+")
((((triple6) -> (rule3 % int2)) triple11) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The mouse is not big.
False
4
inv-proof
[(((((triple6) -> rule3) triple11) -> rule1))]
("mouse" "is" "big" "-")
((((triple6) -> (rule3 % int2)) triple11) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The mouse visits the mouse.
True
5
proof
[(((((((triple6) -> rule3) triple11) -> rule1)) -> rule2))]
("mouse" "visits" "mouse" "+")
((((((triple6) -> (rule3 % int3)) triple11) -> (rule1 % int2))) -> (rule2 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The mouse does not visit the mouse.
False
5
inv-proof
[(((((((triple6) -> rule3) triple11) -> rule1)) -> rule2))]
("mouse" "visits" "mouse" "-")
((((((triple6) -> (rule3 % int3)) triple11) -> (rule1 % int2))) -> (rule2 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The tiger does not visit the mouse.
Unknown
inv-rconc
[@1: The tiger visits the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "visits" "mouse" "-")
The lion visits the mouse.
Unknown
rconc
[@1: The lion visits the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "mouse" "+")
The cat does not visit the mouse.
Unknown
inv-rconc
[@1: The cat visits the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "mouse" "-")
The lion visits the cat.
Unknown
random
[@0: The lion visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cat" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The cat needs the lion.
Unknown
random
[@0: The cat needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "lion" "+")
@0: The cat eats the lion.[(triple1)] The cat eats the mouse.[(triple2)] The cat eats the tiger.[(triple3)] The cat is blue.[(triple4)] The cat is red.[(triple5)] The cat needs the mouse.[(triple6)] The cat visits the lion.[(triple7)] The cat visits the tiger.[(triple8)] The lion eats the mouse.[(triple9)] The lion is blue.[(triple10)] The lion is cold.[(triple11)] The mouse needs the lion.[(triple12)] The mouse needs the tiger.[(triple13)] The tiger eats the cat.[(triple14)] The tiger eats the mouse.[(triple15)] @1: The mouse eats the lion.[(((triple6) -> rule3))] @2: The mouse is big.[(((((triple6) -> rule3) triple11) -> rule1))] @3: The mouse visits the mouse.[(((((((triple6) -> rule3) triple11) -> rule1)) -> rule2))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple2
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple3
The cat is blue.
("cat" "is" "blue" "+")
triple4
The cat is red.
("cat" "is" "red" "+")
triple5
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple6
The cat visits the lion.
("cat" "visits" "lion" "+")
triple7
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple8
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple9
The lion is blue.
("lion" "is" "blue" "+")
triple10
The lion is cold.
("lion" "is" "cold" "+")
triple11
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple12
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple13
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple14
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple15
The mouse eats the lion.
("mouse" "eats" "lion" "+")
((triple6) -> (rule3 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
((((triple6) -> (rule3 % int2)) triple11) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((((((triple6) -> (rule3 % int3)) triple11) -> (rule1 % int2))) -> (rule2 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3