The bear likes the rabbit. The cow needs the rabbit. The rabbit likes the cow. The squirrel is round. If something needs the rabbit then it needs the squirrel. If the cow is red and the cow likes the rabbit then the cow is cold. If something needs the rabbit and the rabbit is red then the rabbit is round. If something eats the bear then the bear is kind. If something likes the rabbit and it needs the rabbit then the rabbit eats the bear. If something eats the squirrel and the squirrel likes the rabbit then it likes the bear. If something likes the squirrel and it likes the cow then the cow is cold. If something needs the squirrel then the squirrel needs the rabbit.
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If something needs the rabbit then it needs the squirrel.
((("something" "needs" "rabbit" "+")) -> ("something" "needs" "squirrel" "+"))
If the cow is red and the cow likes the rabbit then the cow is cold.
((("cow" "is" "red" "+") ("cow" "likes" "rabbit" "+")) -> ("cow" "is" "cold" "+"))
If something needs the rabbit and the rabbit is red then the rabbit is round.
((("something" "needs" "rabbit" "+") ("rabbit" "is" "red" "+")) -> ("rabbit" "is" "round" "+"))
If something eats the bear then the bear is kind.
((("something" "eats" "bear" "+")) -> ("bear" "is" "kind" "+"))
If something likes the rabbit and it needs the rabbit then the rabbit eats the bear.
((("something" "likes" "rabbit" "+") ("something" "needs" "rabbit" "+")) -> ("rabbit" "eats" "bear" "+"))
If something eats the squirrel and the squirrel likes the rabbit then it likes the bear.
((("something" "eats" "squirrel" "+") ("squirrel" "likes" "rabbit" "+")) -> ("something" "likes" "bear" "+"))
If something likes the squirrel and it likes the cow then the cow is cold.
((("something" "likes" "squirrel" "+") ("something" "likes" "cow" "+")) -> ("cow" "is" "cold" "+"))
If something needs the squirrel then the squirrel needs the rabbit.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "needs" "rabbit" "+"))
The squirrel is round.
True
1
proof
[(triple4)]
("squirrel" "is" "round" "+")
triple4
The squirrel is not round.
False
1
inv-proof
[(triple4)]
("squirrel" "is" "round" "-")
triple4
The cow needs the squirrel.
True
2
proof
[(((triple2) -> rule1))]
("cow" "needs" "squirrel" "+")
((triple2) -> (rule1 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow does not need the squirrel.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "needs" "squirrel" "-")
((triple2) -> (rule1 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The squirrel needs the rabbit.
True
3
proof
[(((((triple2) -> rule1)) -> rule8))]
("squirrel" "needs" "rabbit" "+")
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The squirrel does not need the rabbit.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule8))]
("squirrel" "needs" "rabbit" "-")
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The squirrel needs the squirrel.
True
4
proof
[(((((((triple2) -> rule1)) -> rule8)) -> rule1))]
("squirrel" "needs" "squirrel" "+")
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3
The squirrel does not need the squirrel.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule8)) -> rule1))]
("squirrel" "needs" "squirrel" "-")
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3
The cow is not cold.
Unknown
inv-rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "cold" "-")
The cow likes the bear.
Unknown
rconc
[@1: The cow likes the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "likes" "bear" "+")
The squirrel does not like the bear.
Unknown
inv-rconc
[@1: The squirrel likes the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "likes" "bear" "-")
The rabbit is round.
Unknown
rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "round" "+")
The rabbit does not need the cow.
Unknown
inv-random
[@0: The rabbit needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "cow" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
The bear eats the squirrel.
Unknown
random
[@0: The bear eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "squirrel" "+")
@0: The bear likes the rabbit.[(triple1)] The cow needs the rabbit.[(triple2)] The rabbit likes the cow.[(triple3)] The squirrel is round.[(triple4)] @1: The cow needs the squirrel.[(((triple2) -> rule1))] @2: The squirrel needs the rabbit.[(((((triple2) -> rule1)) -> rule8))] @3: The squirrel needs the squirrel.[(((((((triple2) -> rule1)) -> rule8)) -> rule1))]
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple2
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple3
The squirrel is round.
("squirrel" "is" "round" "+")
triple4
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
((triple2) -> (rule1 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3