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