The rabbit likes the squirrel. The rabbit visits the squirrel. The squirrel visits the rabbit. If someone likes the squirrel then they eat the rabbit. If someone is young and big then they like the squirrel. If someone visits the squirrel and they like the rabbit then the squirrel is young. If the squirrel eats the rabbit then the squirrel is young. Kind people are cold. If the squirrel visits the rabbit and the rabbit likes the squirrel then the rabbit eats the squirrel. If someone visits the squirrel then the squirrel visits the rabbit. If someone visits the rabbit then they eat the rabbit.
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If someone likes the squirrel then they eat the rabbit.
((("someone" "likes" "squirrel" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone is young and big then they like the squirrel.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone visits the squirrel and they like the rabbit then the squirrel is young.
((("someone" "visits" "squirrel" "+") ("someone" "likes" "rabbit" "+")) -> ("squirrel" "is" "young" "+"))
If the squirrel eats the rabbit then the squirrel is young.
((("squirrel" "eats" "rabbit" "+")) -> ("squirrel" "is" "young" "+"))
Kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If the squirrel visits the rabbit and the rabbit likes the squirrel then the rabbit eats the squirrel.
((("squirrel" "visits" "rabbit" "+") ("rabbit" "likes" "squirrel" "+")) -> ("rabbit" "eats" "squirrel" "+"))
If someone visits the squirrel then the squirrel visits the rabbit.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "visits" "rabbit" "+"))
If someone visits the rabbit then they eat the rabbit.
((("someone" "visits" "rabbit" "+")) -> ("someone" "eats" "rabbit" "+"))
The squirrel visits the rabbit.
True
1
proof
[(triple3 OR ((triple2) -> rule7))]
("squirrel" "visits" "rabbit" "+")
triple3
((triple2) -> (rule7 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The rabbit does not like the squirrel.
False
1
inv-proof
[(triple1)]
("rabbit" "likes" "squirrel" "-")
triple1
The rabbit eats the rabbit.
True
2
proof
[(((triple1) -> rule1))]
("rabbit" "eats" "rabbit" "+")
((triple1) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The squirrel does not eat the rabbit.
False
2
inv-proof
[(((triple3) -> rule8) OR ((((triple2) -> rule7)) -> rule8))]
("squirrel" "eats" "rabbit" "-")
((triple3) -> (rule8 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
The squirrel is young.
True
3
proof
[(((((triple3) -> rule8)) -> rule4) OR ((((((triple2) -> rule7)) -> rule8)) -> rule4))]
("squirrel" "is" "young" "+")
((((triple3) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int2
((((((triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int3
The squirrel is not young.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule4) OR ((((((triple2) -> rule7)) -> rule8)) -> rule4))]
("squirrel" "is" "young" "-")
((((triple3) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int2
((((((triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int3
The squirrel is not cold.
Unknown
inv-rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "cold" "-")
The rabbit is cold.
Unknown
rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "cold" "+")
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
@0: The rabbit likes the squirrel.[(triple1)] The rabbit visits the squirrel.[(triple2)] The squirrel visits the rabbit.[(triple3 OR ((triple2) -> rule7))] @1: The rabbit eats the rabbit.[(((triple1) -> rule1))] The rabbit eats the squirrel.[(((triple3 triple1) -> rule6) OR ((((triple2) -> rule7) triple1) -> rule6))] The squirrel eats the rabbit.[(((triple3) -> rule8) OR ((((triple2) -> rule7)) -> rule8))] @2: The squirrel is young.[(((((triple3) -> rule8)) -> rule4) OR ((((((triple2) -> rule7)) -> rule8)) -> rule4))]
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple3
((triple2) -> (rule7 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple1) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
((triple3 triple1) -> (rule6 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
((((triple2) -> (rule7 % int2)) triple1) -> (rule6 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
((triple3) -> (rule8 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
((((triple3) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int2
((((((triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int3