The dog is red. The rabbit is red. The squirrel is nice. If the rabbit sees the dog and the dog is nice then the dog sees the rabbit. If the rabbit is cold then the rabbit needs the squirrel. If someone sees the squirrel then the squirrel sees the dog. If someone is cold then they need the squirrel. If someone eats the squirrel and they need the squirrel then they see the rabbit. Nice people are cold.
The dog is red.
("dog" "is" "red" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
If the rabbit sees the dog and the dog is nice then the dog sees the rabbit.
((("rabbit" "sees" "dog" "+") ("dog" "is" "nice" "+")) -> ("dog" "sees" "rabbit" "+"))
If the rabbit is cold then the rabbit needs the squirrel.
((("rabbit" "is" "cold" "+")) -> ("rabbit" "needs" "squirrel" "+"))
If someone sees the squirrel then the squirrel sees the dog.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "sees" "dog" "+"))
If someone is cold then they need the squirrel.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone eats the squirrel and they need the squirrel then they see the rabbit.
((("someone" "eats" "squirrel" "+") ("someone" "needs" "squirrel" "+")) -> ("someone" "sees" "rabbit" "+"))
Nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
The squirrel is nice.
True
1
proof
[(triple3)]
("squirrel" "is" "nice" "+")
triple3
The dog is not red.
False
1
inv-proof
[(triple1)]
("dog" "is" "red" "-")
triple1
The squirrel is cold.
True
2
proof
[(((triple3) -> rule6))]
("squirrel" "is" "cold" "+")
((triple3) -> (rule6 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is not cold.
False
2
inv-proof
[(((triple3) -> rule6))]
("squirrel" "is" "cold" "-")
((triple3) -> (rule6 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel needs the squirrel.
True
3
proof
[(((((triple3) -> rule6)) -> rule4))]
("squirrel" "needs" "squirrel" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel does not need the squirrel.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule4))]
("squirrel" "needs" "squirrel" "-")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The dog does not see the rabbit.
Unknown
inv-rconc
[@1: The dog sees the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "rabbit" "-")
The rabbit needs the squirrel.
Unknown
rconc
[@2: The rabbit needs the squirrel.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("rabbit" "needs" "squirrel" "+")
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The dog eats the squirrel.
Unknown
random
[@0: The dog eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "squirrel" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
@0: The dog is red.[(triple1)] The rabbit is red.[(triple2)] The squirrel is nice.[(triple3)] @1: The squirrel is cold.[(((triple3) -> rule6))] @2: The squirrel needs the squirrel.[(((((triple3) -> rule6)) -> rule4))]
The dog is red.
("dog" "is" "red" "+")
triple1
The rabbit is red.
("rabbit" "is" "red" "+")
triple2
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple3
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple3) -> (rule6 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2