The cow sees the rabbit. The cow sees the squirrel. The rabbit chases the cow. The rabbit is red. The rabbit is round. The rabbit needs the squirrel. The squirrel is not big. If the rabbit is big then the rabbit sees the squirrel. If someone sees the rabbit then the rabbit does not need the cow. If someone sees the squirrel then they chase the cow. If someone needs the cow then they chase the cow. If the squirrel chases the rabbit and the rabbit is big then the rabbit needs the squirrel. If someone needs the squirrel and they see the squirrel then they are cold. If someone sees the rabbit and the rabbit does not chase the cow then the rabbit sees the cow. If the rabbit does not need the cow then the cow needs the squirrel.
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The squirrel is not big.
("squirrel" "is" "big" "-")
If the rabbit is big then the rabbit sees the squirrel.
((("rabbit" "is" "big" "+")) -> ("rabbit" "sees" "squirrel" "+"))
If someone sees the rabbit then the rabbit does not need the cow.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "needs" "cow" "-"))
If someone sees the squirrel then they chase the cow.
((("someone" "sees" "squirrel" "+")) -> ("someone" "chases" "cow" "+"))
If someone needs the cow then they chase the cow.
((("someone" "needs" "cow" "+")) -> ("someone" "chases" "cow" "+"))
If the squirrel chases the rabbit and the rabbit is big then the rabbit needs the squirrel.
((("squirrel" "chases" "rabbit" "+") ("rabbit" "is" "big" "+")) -> ("rabbit" "needs" "squirrel" "+"))
If someone needs the squirrel and they see the squirrel then they are cold.
((("someone" "needs" "squirrel" "+") ("someone" "sees" "squirrel" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the rabbit and the rabbit does not chase the cow then the rabbit sees the cow.
((("someone" "sees" "rabbit" "+") ("rabbit" "chases" "cow" "~")) -> ("rabbit" "sees" "cow" "+"))
If the rabbit does not need the cow then the cow needs the squirrel.
((("rabbit" "needs" "cow" "~")) -> ("cow" "needs" "squirrel" "+"))
The rabbit chases the cow.
True
1
proof
[(triple3)]
("rabbit" "chases" "cow" "+")
triple3
The rabbit does not need the squirrel.
False
1
inv-proof
[(triple6)]
("rabbit" "needs" "squirrel" "-")
triple6
The cow chases the cow.
True
2
proof
[(((triple2) -> rule3))]
("cow" "chases" "cow" "+")
((triple2) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow does not chase the cow.
False
2
inv-proof
[(((triple2) -> rule3))]
("cow" "chases" "cow" "-")
((triple2) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow needs the squirrel.
True
3
proof
[(((((triple1) -> rule2)) -> rule8))]
("cow" "needs" "squirrel" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The rabbit does not need the cow.
("rabbit" "needs" "cow" "-")
int2
The cow does not need the squirrel.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule8))]
("cow" "needs" "squirrel" "-")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The rabbit does not need the cow.
("rabbit" "needs" "cow" "-")
int2
The cow is cold.
True
5
proof
[(((((((triple1) -> rule2)) -> rule8) triple2) -> rule6))]
("cow" "is" "cold" "+")
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2)) triple2) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The rabbit does not need the cow.
("rabbit" "needs" "cow" "-")
int3
The cow is not cold.
False
5
inv-proof
[(((((((triple1) -> rule2)) -> rule8) triple2) -> rule6))]
("cow" "is" "cold" "-")
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2)) triple2) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The rabbit does not need the cow.
("rabbit" "needs" "cow" "-")
int3
The squirrel is not cold.
Unknown
inv-rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "cold" "-")
The rabbit is cold.
Unknown
rconc
[@2: The rabbit is cold.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("rabbit" "is" "cold" "+")
The rabbit does not see the squirrel.
Unknown
inv-rconc
[@1: The rabbit sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "sees" "squirrel" "-")
The rabbit sees the cow.
Unknown
rconc
[@1: The rabbit sees the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "sees" "cow" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
The squirrel does not need the rabbit.
Unknown
inv-random
[@0: The squirrel needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "rabbit" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
@0: The cow sees the rabbit.[(triple1)] The cow sees the squirrel.[(triple2)] The rabbit chases the cow.[(triple3)] The rabbit is red.[(triple4)] The rabbit is round.[(triple5)] The rabbit needs the squirrel.[(triple6)] The squirrel is not big.[(triple7)] @1: The cow chases the cow.[(((triple2) -> rule3))] The rabbit does not need the cow.[(((triple1) -> rule2))] @2: The cow needs the squirrel.[(((((triple1) -> rule2)) -> rule8))] @3: The cow is cold.[(((((((triple1) -> rule2)) -> rule8) triple2) -> rule6))]
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple2
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple3
The rabbit is red.
("rabbit" "is" "red" "+")
triple4
The rabbit is round.
("rabbit" "is" "round" "+")
triple5
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple6
The squirrel is not big.
("squirrel" "is" "big" "-")
triple7
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple2) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The rabbit does not need the cow.
("rabbit" "needs" "cow" "-")
((triple1) -> (rule2 % int1))
The rabbit does not need the cow.
("rabbit" "needs" "cow" "-")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The rabbit does not need the cow.
("rabbit" "needs" "cow" "-")
int2
The cow is cold.
("cow" "is" "cold" "+")
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2)) triple2) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The rabbit does not need the cow.
("rabbit" "needs" "cow" "-")
int3