The rabbit is nice. The squirrel chases the rabbit. The squirrel sees the rabbit. If someone visits the rabbit then they are red. If someone sees the rabbit then the rabbit chases the squirrel. If someone is kind then they see the squirrel. If someone sees the rabbit and the rabbit sees the squirrel then the rabbit is nice. If someone chases the squirrel then the squirrel is red. All cold people are red. If someone chases the squirrel and the squirrel is red then they visit the squirrel. If someone visits the squirrel then the squirrel is nice.
The rabbit is nice.
("rabbit" "is" "nice" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If someone visits the rabbit then they are red.
((("someone" "visits" "rabbit" "+")) -> ("someone" "is" "red" "+"))
If someone sees the rabbit then the rabbit chases the squirrel.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "chases" "squirrel" "+"))
If someone is kind then they see the squirrel.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone sees the rabbit and the rabbit sees the squirrel then the rabbit is nice.
((("someone" "sees" "rabbit" "+") ("rabbit" "sees" "squirrel" "+")) -> ("rabbit" "is" "nice" "+"))
If someone chases the squirrel then the squirrel is red.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "is" "red" "+"))
All cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone chases the squirrel and the squirrel is red then they visit the squirrel.
((("someone" "chases" "squirrel" "+") ("squirrel" "is" "red" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone visits the squirrel then the squirrel is nice.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "is" "nice" "+"))
The squirrel chases the rabbit.
True
1
proof
[(triple2)]
("squirrel" "chases" "rabbit" "+")
triple2
The rabbit is not nice.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "nice" "-")
triple1
The rabbit chases the squirrel.
True
2
proof
[(((triple3) -> rule2))]
("rabbit" "chases" "squirrel" "+")
((triple3) -> (rule2 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit does not chase the squirrel.
False
2
inv-proof
[(((triple3) -> rule2))]
("rabbit" "chases" "squirrel" "-")
((triple3) -> (rule2 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The squirrel is red.
True
3
proof
[(((((triple3) -> rule2)) -> rule5))]
("squirrel" "is" "red" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int2
The squirrel is not red.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule5))]
("squirrel" "is" "red" "-")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int2
The rabbit visits the squirrel.
True
6
proof
[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule5)) -> rule7))]
("rabbit" "visits" "squirrel" "+")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int3
The rabbit does not visit the squirrel.
False
6
inv-proof
[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule5)) -> rule7))]
("rabbit" "visits" "squirrel" "-")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int3
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "red" "-")
The squirrel visits the squirrel.
Unknown
rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "visits" "squirrel" "+")
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The rabbit sees the squirrel.
Unknown
rconc
[@1: The rabbit sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "sees" "squirrel" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
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 rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The rabbit is nice.[(triple1)] The squirrel chases the rabbit.[(triple2)] The squirrel sees the rabbit.[(triple3)] @1: The rabbit chases the squirrel.[(((triple3) -> rule2))] @2: The squirrel is red.[(((((triple3) -> rule2)) -> rule5))] @3: The rabbit visits the squirrel.[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule5)) -> rule7))] @4: The squirrel is nice.[(((((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule5)) -> rule7)) -> rule8))]
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple1
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple3
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
((triple3) -> (rule2 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int3
The squirrel is nice.
("squirrel" "is" "nice" "+")
((((((triple3) -> (rule2 % int4)) ((((triple3) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int4