The rabbit is big. The rabbit is blue. The rabbit is cold. The rabbit is round. The rabbit likes the squirrel. The rabbit needs the squirrel. The rabbit visits the squirrel. The squirrel is cold. The squirrel is kind. The squirrel likes the rabbit. If something needs the squirrel then the squirrel needs the rabbit. If the rabbit is cold then the rabbit is round. If something visits the rabbit and the rabbit needs the squirrel then the rabbit likes the squirrel. If something visits the rabbit then it is round. If something needs the rabbit and the rabbit is cold then it is big. If something is big and kind then it visits the squirrel. If something visits the rabbit then it is round. If the rabbit is kind and the rabbit visits the squirrel then the squirrel likes the rabbit.
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
If something needs the squirrel then the squirrel needs the rabbit.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "needs" "rabbit" "+"))
If the rabbit is cold then the rabbit is round.
((("rabbit" "is" "cold" "+")) -> ("rabbit" "is" "round" "+"))
If something visits the rabbit and the rabbit needs the squirrel then the rabbit likes the squirrel.
((("something" "visits" "rabbit" "+") ("rabbit" "needs" "squirrel" "+")) -> ("rabbit" "likes" "squirrel" "+"))
If something visits the rabbit then it is round.
((("something" "visits" "rabbit" "+")) -> ("something" "is" "round" "+"))
If something needs the rabbit and the rabbit is cold then it is big.
((("something" "needs" "rabbit" "+") ("rabbit" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something is big and kind then it visits the squirrel.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "visits" "squirrel" "+"))
If something visits the rabbit then it is round.
((("something" "visits" "rabbit" "+")) -> ("something" "is" "round" "+"))
If the rabbit is kind and the rabbit visits the squirrel then the squirrel likes the rabbit.
((("rabbit" "is" "kind" "+") ("rabbit" "visits" "squirrel" "+")) -> ("squirrel" "likes" "rabbit" "+"))
The rabbit likes the squirrel.
True
1
proof
[(triple5)]
("rabbit" "likes" "squirrel" "+")
triple5
The rabbit is not blue.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "blue" "-")
triple2
The squirrel needs the rabbit.
True
2
proof
[(((triple6) -> rule1))]
("squirrel" "needs" "rabbit" "+")
((triple6) -> (rule1 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel does not need the rabbit.
False
2
inv-proof
[(((triple6) -> rule1))]
("squirrel" "needs" "rabbit" "-")
((triple6) -> (rule1 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel is big.
True
4
proof
[(((((triple6) -> rule1) triple3) -> rule5))]
("squirrel" "is" "big" "+")
((((triple6) -> (rule1 % int2)) triple3) -> (rule5 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int2
The squirrel is not big.
False
4
inv-proof
[(((((triple6) -> rule1) triple3) -> rule5))]
("squirrel" "is" "big" "-")
((((triple6) -> (rule1 % int2)) triple3) -> (rule5 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int2
The squirrel visits the squirrel.
True
6
proof
[(((((((triple6) -> rule1) triple3) -> rule5) triple9) -> rule6))]
("squirrel" "visits" "squirrel" "+")
((((((triple6) -> (rule1 % int3)) triple3) -> (rule5 % int2)) triple9) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int3
The squirrel does not visit the squirrel.
False
6
inv-proof
[(((((((triple6) -> rule1) triple3) -> rule5) triple9) -> rule6))]
("squirrel" "visits" "squirrel" "-")
((((((triple6) -> (rule1 % int3)) triple3) -> (rule5 % int2)) triple9) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int3
The squirrel is not round.
Unknown
inv-rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "round" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The squirrel visits the rabbit.
Unknown
random
[@0: The squirrel visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "rabbit" "+")
@0: The rabbit is big.[(triple1)] The rabbit is blue.[(triple2)] The rabbit is cold.[(triple3)] The rabbit is round.[(triple4 OR ((triple3) -> rule2))] The rabbit likes the squirrel.[(triple5)] The rabbit needs the squirrel.[(triple6)] The rabbit visits the squirrel.[(triple7)] The squirrel is cold.[(triple8)] The squirrel is kind.[(triple9)] The squirrel likes the rabbit.[(triple10)] @1: The squirrel needs the rabbit.[(((triple6) -> rule1))] @2: The squirrel is big.[(((((triple6) -> rule1) triple3) -> rule5))] @3: The squirrel visits the squirrel.[(((((((triple6) -> rule1) triple3) -> rule5) triple9) -> rule6))]
The rabbit is big.
("rabbit" "is" "big" "+")
triple1
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple2
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple3
The rabbit is round.
("rabbit" "is" "round" "+")
triple4
((triple3) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple5
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple6
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple7
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple8
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple9
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple10
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
((triple6) -> (rule1 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((((triple6) -> (rule1 % int2)) triple3) -> (rule5 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((((((triple6) -> (rule1 % int3)) triple3) -> (rule5 % int2)) triple9) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int3