The cat eats the mouse. The cat eats the tiger. The cat is not kind. The cat does not need the mouse. The cat visits the tiger. The mouse is not nice. The mouse is young. The mouse needs the tiger. The tiger is not blue. The tiger is young. The tiger needs the cat. The tiger visits the cat. If something eats the tiger and the tiger visits the cat then the tiger eats the mouse. If something is kind then it needs the mouse.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is not kind.
("cat" "is" "kind" "-")
The cat does not need the mouse.
("cat" "needs" "mouse" "-")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The mouse is not nice.
("mouse" "is" "nice" "-")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger is not blue.
("tiger" "is" "blue" "-")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If something eats the tiger and the tiger visits the cat then the tiger eats the mouse.
((("something" "eats" "tiger" "+") ("tiger" "visits" "cat" "+")) -> ("tiger" "eats" "mouse" "+"))
If something is kind then it needs the mouse.
((("something" "is" "kind" "+")) -> ("something" "needs" "mouse" "+"))
The cat visits the tiger.
True
1
proof
[(triple5)]
("cat" "visits" "tiger" "+")
triple5
The cat does not visit the tiger.
False
1
inv-proof
[(triple5)]
("cat" "visits" "tiger" "-")
triple5
The tiger eats the mouse.
True
3
proof
[(((triple2 triple12) -> rule1))]
("tiger" "eats" "mouse" "+")
((triple2 triple12) -> (rule1 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger does not eat the mouse.
False
3
inv-proof
[(((triple2 triple12) -> rule1))]
("tiger" "eats" "mouse" "-")
((triple2 triple12) -> (rule1 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The tiger needs the mouse.
Unknown
rconc
[@1: The tiger needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "needs" "mouse" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The mouse visits the cat.
Unknown
random
[@0: The mouse visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cat" "+")
@0: The cat does not need the mouse.[(triple4)] The cat eats the mouse.[(triple1)] The cat eats the tiger.[(triple2)] The cat is not kind.[(triple3)] The cat visits the tiger.[(triple5)] The mouse is not nice.[(triple6)] The mouse is young.[(triple7)] The mouse needs the tiger.[(triple8)] The tiger is not blue.[(triple9)] The tiger is young.[(triple10)] The tiger needs the cat.[(triple11)] The tiger visits the cat.[(triple12)] @1: The tiger eats the mouse.[(((triple2 triple12) -> rule1))]
The cat does not need the mouse.
("cat" "needs" "mouse" "-")
triple4
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple2
The cat is not kind.
("cat" "is" "kind" "-")
triple3
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple5
The mouse is not nice.
("mouse" "is" "nice" "-")
triple6
The mouse is young.
("mouse" "is" "young" "+")
triple7
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple8
The tiger is not blue.
("tiger" "is" "blue" "-")
triple9
The tiger is young.
("tiger" "is" "young" "+")
triple10
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple11
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple12
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((triple2 triple12) -> (rule1 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1