The bear chases the squirrel. The rabbit visits the squirrel. The squirrel visits the rabbit. If something chases the squirrel then it is nice. If something chases the squirrel and it is nice then the squirrel eats the rabbit. If something eats the rabbit then the rabbit is kind.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If something chases the squirrel then it is nice.
((("something" "chases" "squirrel" "+")) -> ("something" "is" "nice" "+"))
If something chases the squirrel and it is nice then the squirrel eats the rabbit.
((("something" "chases" "squirrel" "+") ("something" "is" "nice" "+")) -> ("squirrel" "eats" "rabbit" "+"))
If something eats the rabbit then the rabbit is kind.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "is" "kind" "+"))
The rabbit visits the squirrel.
True
1
proof
[(triple2)]
("rabbit" "visits" "squirrel" "+")
triple2
The rabbit does not visit the squirrel.
False
1
inv-proof
[(triple2)]
("rabbit" "visits" "squirrel" "-")
triple2
The bear is nice.
True
2
proof
[(((triple1) -> rule1))]
("bear" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "is" "nice" "-")
((triple1) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The squirrel eats the rabbit.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("squirrel" "eats" "rabbit" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The squirrel does not eat the rabbit.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("squirrel" "eats" "rabbit" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The rabbit is kind.
True
5
proof
[(((((triple1 ((triple1) -> rule1)) -> rule2)) -> rule3))]
("rabbit" "is" "kind" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The rabbit is not kind.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule2)) -> rule3))]
("rabbit" "is" "kind" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "nice" "-")
The squirrel is nice.
Unknown
rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "nice" "+")
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 visits the bear.
Unknown
random
[@0: The squirrel visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "bear" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
@0: The bear chases the squirrel.[(triple1)] The rabbit visits the squirrel.[(triple2)] The squirrel visits the rabbit.[(triple3)] @1: The bear is nice.[(((triple1) -> rule1))] @2: The squirrel eats the rabbit.[(((triple1 ((triple1) -> rule1)) -> rule2))] @3: The rabbit is kind.[(((((triple1 ((triple1) -> rule1)) -> rule2)) -> rule3))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple3
The bear is nice.
("bear" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3