The cat is big. The cat is round. The cat visits the mouse. The mouse eats the cat. The mouse is round. The mouse is young. The mouse needs the rabbit. The mouse visits the rabbit. The rabbit eats the cat. The rabbit visits the mouse. If someone visits the rabbit and they are big then the rabbit needs the mouse. If someone visits the rabbit then they are young. If someone eats the rabbit then they need the rabbit. If someone visits the rabbit and the rabbit visits the mouse then the rabbit visits the cat. If someone eats the mouse and the mouse is young then they need the mouse. If someone is big then they visit the rabbit. If someone needs the mouse then the mouse eats the cat. If someone is round then they need the cat.
The cat is big.
("cat" "is" "big" "+")
The cat is round.
("cat" "is" "round" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If someone visits the rabbit and they are big then the rabbit needs the mouse.
((("someone" "visits" "rabbit" "+") ("someone" "is" "big" "+")) -> ("rabbit" "needs" "mouse" "+"))
If someone visits the rabbit then they are young.
((("someone" "visits" "rabbit" "+")) -> ("someone" "is" "young" "+"))
If someone eats the rabbit then they need the rabbit.
((("someone" "eats" "rabbit" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone visits the rabbit and the rabbit visits the mouse then the rabbit visits the cat.
((("someone" "visits" "rabbit" "+") ("rabbit" "visits" "mouse" "+")) -> ("rabbit" "visits" "cat" "+"))
If someone eats the mouse and the mouse is young then they need the mouse.
((("someone" "eats" "mouse" "+") ("mouse" "is" "young" "+")) -> ("someone" "needs" "mouse" "+"))
If someone is big then they visit the rabbit.
((("someone" "is" "big" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone needs the mouse then the mouse eats the cat.
((("someone" "needs" "mouse" "+")) -> ("mouse" "eats" "cat" "+"))
If someone is round then they need the cat.
((("someone" "is" "round" "+")) -> ("someone" "needs" "cat" "+"))
The mouse needs the rabbit.
True
1
proof
[(triple7)]
("mouse" "needs" "rabbit" "+")
triple7
The mouse does not visit the rabbit.
False
1
inv-proof
[(triple8)]
("mouse" "visits" "rabbit" "-")
triple8
The cat needs the cat.
True
2
proof
[(((triple2) -> rule8))]
("cat" "needs" "cat" "+")
((triple2) -> (rule8 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not visit the rabbit.
False
2
inv-proof
[(((triple1) -> rule6))]
("cat" "visits" "rabbit" "-")
((triple1) -> (rule6 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is young.
True
3
proof
[(((((triple1) -> rule6)) -> rule2))]
("cat" "is" "young" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The rabbit does not need the mouse.
False
4
inv-proof
[(((((triple1) -> rule6) triple1) -> rule1))]
("rabbit" "needs" "mouse" "-")
((((triple1) -> (rule6 % int2)) triple1) -> (rule1 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit visits the rabbit.
Unknown
rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "visits" "rabbit" "+")
The cat does not need the mouse.
Unknown
inv-rconc
[@1: The cat needs the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "needs" "mouse" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
@0: The cat is big.[(triple1)] The cat is round.[(triple2)] The cat visits the mouse.[(triple3)] The mouse eats the cat.[(triple4 OR ((((((triple1) -> rule6) triple1) -> rule1)) -> rule7))] The mouse is round.[(triple5)] The mouse is young.[(triple6 OR ((triple8) -> rule2))] The mouse needs the rabbit.[(triple7)] The mouse visits the rabbit.[(triple8)] The rabbit eats the cat.[(triple9)] The rabbit visits the mouse.[(triple10)] @1: The cat needs the cat.[(((triple2) -> rule8))] The cat visits the rabbit.[(((triple1) -> rule6))] The mouse needs the cat.[(((triple5) -> rule8))] The rabbit visits the cat.[(((triple8 triple10) -> rule4) OR ((((triple1) -> rule6) triple10) -> rule4))] @2: The cat is young.[(((((triple1) -> rule6)) -> rule2))] The rabbit needs the mouse.[(((((triple1) -> rule6) triple1) -> rule1))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is round.
("cat" "is" "round" "+")
triple2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple3
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple4
((((((triple1) -> (rule6 % int3)) triple1) -> (rule1 % int2))) -> (rule7 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int3
The mouse is round.
("mouse" "is" "round" "+")
triple5
The mouse is young.
("mouse" "is" "young" "+")
triple6
((triple8) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple7
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple8
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple9
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple10
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple2) -> (rule8 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
((triple1) -> (rule6 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
((triple5) -> (rule8 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
((triple8 triple10) -> (rule4 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
((((triple1) -> (rule6 % int2)) triple10) -> (rule4 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat is young.
("cat" "is" "young" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule1 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2