The cat chases the mouse. The cat eats the mouse. The cat is big. The cat is cold. The cat is kind. The cat is round. The cat is young. The cat needs the mouse. The mouse chases the cat. The mouse eats the cat. The mouse is cold. The mouse is kind. The mouse is round. The mouse is young. The mouse needs the cat. If something eats the mouse then it is round. If the cat is round then the cat needs the mouse. If something needs the cat then the cat is kind. If something is kind and it eats the mouse then it needs the cat. If something chases the mouse and the mouse eats the cat then the mouse chases the cat. If something eats the mouse then it is big.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
If something eats the mouse then it is round.
((("something" "eats" "mouse" "+")) -> ("something" "is" "round" "+"))
If the cat is round then the cat needs the mouse.
((("cat" "is" "round" "+")) -> ("cat" "needs" "mouse" "+"))
If something needs the cat then the cat is kind.
((("something" "needs" "cat" "+")) -> ("cat" "is" "kind" "+"))
If something is kind and it eats the mouse then it needs the cat.
((("something" "is" "kind" "+") ("something" "eats" "mouse" "+")) -> ("something" "needs" "cat" "+"))
If something chases the mouse and the mouse eats the cat then the mouse chases the cat.
((("something" "chases" "mouse" "+") ("mouse" "eats" "cat" "+")) -> ("mouse" "chases" "cat" "+"))
If something eats the mouse then it is big.
((("something" "eats" "mouse" "+")) -> ("something" "is" "big" "+"))
The cat chases the mouse.
True
1
proof
[(triple1)]
("cat" "chases" "mouse" "+")
triple1
The cat does not eat the mouse.
False
1
inv-proof
[(triple2)]
("cat" "eats" "mouse" "-")
triple2
The cat needs the cat.
True
3
proof
[(((triple5 triple2) -> rule4) OR ((((triple15) -> rule3) triple2) -> rule4))]
("cat" "needs" "cat" "+")
((triple5 triple2) -> (rule4 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
((((triple15) -> (rule3 % int2)) triple2) -> (rule4 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat does not need the cat.
False
3
inv-proof
[(((triple5 triple2) -> rule4) OR ((((triple15) -> rule3) triple2) -> rule4))]
("cat" "needs" "cat" "-")
((triple5 triple2) -> (rule4 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
((((triple15) -> (rule3 % int2)) triple2) -> (rule4 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "big" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat chases the mouse.[(triple1)] The cat eats the mouse.[(triple2)] The cat is big.[(triple3 OR ((triple2) -> rule6))] The cat is cold.[(triple4)] The cat is kind.[(triple5 OR ((triple15) -> rule3))] The cat is round.[(triple6 OR ((triple2) -> rule1))] The cat is young.[(triple7)] The cat needs the mouse.[(triple8 OR ((triple6) -> rule2) OR ((((triple2) -> rule1)) -> rule2))] The mouse chases the cat.[(triple9 OR ((triple1 triple10) -> rule5))] The mouse eats the cat.[(triple10)] The mouse is cold.[(triple11)] The mouse is kind.[(triple12)] The mouse is round.[(triple13)] The mouse is young.[(triple14)] The mouse needs the cat.[(triple15)] @1: The cat needs the cat.[(((triple5 triple2) -> rule4) OR ((((triple15) -> rule3) triple2) -> rule4))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple2
The cat is big.
("cat" "is" "big" "+")
triple3
((triple2) -> (rule6 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
triple4
The cat is kind.
("cat" "is" "kind" "+")
triple5
((triple15) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is round.
("cat" "is" "round" "+")
triple6
((triple2) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is young.
("cat" "is" "young" "+")
triple7
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple8
((triple6) -> (rule2 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple9
((triple1 triple10) -> (rule5 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple10
The mouse is cold.
("mouse" "is" "cold" "+")
triple11
The mouse is kind.
("mouse" "is" "kind" "+")
triple12
The mouse is round.
("mouse" "is" "round" "+")
triple13
The mouse is young.
("mouse" "is" "young" "+")
triple14
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple15
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple5 triple2) -> (rule4 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
((((triple15) -> (rule3 % int2)) triple2) -> (rule4 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2