The cat eats the mouse. The cat eats the squirrel. The cat likes the mouse. The cat sees the mouse. The mouse eats the cat. The mouse eats the squirrel. The mouse is kind. The mouse is young. The mouse likes the cat. The mouse likes the squirrel. The mouse sees the cat. The mouse sees the squirrel. The squirrel eats the cat. The squirrel is round. The squirrel is young. The squirrel sees the mouse. If someone likes the cat then the cat is cold. If someone eats the squirrel then the squirrel likes the cat. If someone eats the squirrel and the squirrel likes the cat then the cat likes the mouse. If the squirrel likes the mouse and the mouse is cold then the mouse eats the squirrel. If someone is round and young then they see the mouse. If someone is red and they like the cat then the cat is red. If someone sees the cat and the cat is cold then they like the mouse. If someone is red and they like the mouse then they are young.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If someone likes the cat then the cat is cold.
((("someone" "likes" "cat" "+")) -> ("cat" "is" "cold" "+"))
If someone eats the squirrel then the squirrel likes the cat.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "likes" "cat" "+"))
If someone eats the squirrel and the squirrel likes the cat then the cat likes the mouse.
((("someone" "eats" "squirrel" "+") ("squirrel" "likes" "cat" "+")) -> ("cat" "likes" "mouse" "+"))
If the squirrel likes the mouse and the mouse is cold then the mouse eats the squirrel.
((("squirrel" "likes" "mouse" "+") ("mouse" "is" "cold" "+")) -> ("mouse" "eats" "squirrel" "+"))
If someone is round and young then they see the mouse.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "sees" "mouse" "+"))
If someone is red and they like the cat then the cat is red.
((("someone" "is" "red" "+") ("someone" "likes" "cat" "+")) -> ("cat" "is" "red" "+"))
If someone sees the cat and the cat is cold then they like the mouse.
((("someone" "sees" "cat" "+") ("cat" "is" "cold" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is red and they like the mouse then they are young.
((("someone" "is" "red" "+") ("someone" "likes" "mouse" "+")) -> ("someone" "is" "young" "+"))
The squirrel is young.
True
1
proof
[(triple15)]
("squirrel" "is" "young" "+")
triple15
The mouse is not kind.
False
1
inv-proof
[(triple7)]
("mouse" "is" "kind" "-")
triple7
The squirrel likes the cat.
True
2
proof
[(((triple2) -> rule2) OR ((triple6) -> rule2))]
("squirrel" "likes" "cat" "+")
((triple2) -> (rule2 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
((triple6) -> (rule2 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
The cat is not cold.
False
2
inv-proof
[(((triple9) -> rule1) OR ((((triple2) -> rule2)) -> rule1) OR ((((triple6) -> rule2)) -> rule1))]
("cat" "is" "cold" "-")
((triple9) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The mouse likes the mouse.
True
4
proof
[(((triple11 ((triple9) -> rule1)) -> rule7) OR ((triple11 ((((triple2) -> rule2)) -> rule1)) -> rule7) OR ((triple11 ((((triple6) -> rule2)) -> rule1)) -> rule7))]
("mouse" "likes" "mouse" "+")
((triple11 ((triple9) -> (rule1 % int2))) -> (rule7 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
((triple11 ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
((triple11 ((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
The mouse does not like the mouse.
False
4
inv-proof
[(((triple11 ((triple9) -> rule1)) -> rule7) OR ((triple11 ((((triple2) -> rule2)) -> rule1)) -> rule7) OR ((triple11 ((((triple6) -> rule2)) -> rule1)) -> rule7))]
("mouse" "likes" "mouse" "-")
((triple11 ((triple9) -> (rule1 % int2))) -> (rule7 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
((triple11 ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
((triple11 ((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
The squirrel does not like the mouse.
Unknown
inv-rconc
[@1: The squirrel likes the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "likes" "mouse" "-")
The cat is red.
Unknown
rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "red" "+")
The cat is not young.
Unknown
inv-rconc
[@2: The cat is young.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("cat" "is" "young" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
@0: The cat eats the mouse.[(triple1)] The cat eats the squirrel.[(triple2)] The cat likes the mouse.[(triple3 OR ((triple2 ((triple2) -> rule2)) -> rule3) OR ((triple2 ((triple6) -> rule2)) -> rule3) OR ((triple6 ((triple2) -> rule2)) -> rule3) OR ((triple6 ((triple6) -> rule2)) -> rule3))] The cat sees the mouse.[(triple4)] The mouse eats the cat.[(triple5)] The mouse eats the squirrel.[(triple6)] The mouse is kind.[(triple7)] The mouse is young.[(triple8)] The mouse likes the cat.[(triple9)] The mouse likes the squirrel.[(triple10)] The mouse sees the cat.[(triple11)] The mouse sees the squirrel.[(triple12)] The squirrel eats the cat.[(triple13)] The squirrel is round.[(triple14)] The squirrel is young.[(triple15)] The squirrel sees the mouse.[(triple16 OR ((triple14 triple15) -> rule5))] @1: The cat is cold.[(((triple9) -> rule1) OR ((((triple2) -> rule2)) -> rule1) OR ((((triple6) -> rule2)) -> rule1))] The squirrel likes the cat.[(((triple2) -> rule2) OR ((triple6) -> rule2))] @2: The mouse likes the mouse.[(((triple11 ((triple9) -> rule1)) -> rule7) OR ((triple11 ((((triple2) -> rule2)) -> rule1)) -> rule7) OR ((triple11 ((((triple6) -> rule2)) -> rule1)) -> rule7))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple3
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
((triple2 ((triple6) -> (rule2 % int2))) -> (rule3 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
((triple6 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
((triple6 ((triple6) -> (rule2 % int2))) -> (rule3 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple4
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple5
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple6
The mouse is kind.
("mouse" "is" "kind" "+")
triple7
The mouse is young.
("mouse" "is" "young" "+")
triple8
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple9
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple10
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple11
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple12
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple13
The squirrel is round.
("squirrel" "is" "round" "+")
triple14
The squirrel is young.
("squirrel" "is" "young" "+")
triple15
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple16
((triple14 triple15) -> (rule5 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
((triple9) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
((triple2) -> (rule2 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
((triple6) -> (rule2 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple11 ((triple9) -> (rule1 % int2))) -> (rule7 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
((triple11 ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
((triple11 ((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3