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