The bald eagle is red. The bald eagle sees the cow. The cow is nice. The cow sees the bald eagle. The lion is nice. The lion is red. The lion sees the squirrel. The squirrel is kind. The squirrel sees the bald eagle. The squirrel sees the lion. If someone is nice and they eat the lion then they chase the lion. If someone is kind and nice then they chase the lion. If someone chases the squirrel and the squirrel sees the bald eagle then the squirrel is nice. If someone sees the bald eagle then they see the squirrel. If the bald eagle sees the squirrel and the squirrel eats the cow then the cow is kind. If someone chases the squirrel and the squirrel eats the lion then they see the lion. If the squirrel chases the lion and the lion eats the cow then the lion sees the bald eagle. If someone is kind and they see the lion then they chase the squirrel.
The bald eagle is red.
("bald eagle" "is" "red" "+")
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If someone is nice and they eat the lion then they chase the lion.
((("someone" "is" "nice" "+") ("someone" "eats" "lion" "+")) -> ("someone" "chases" "lion" "+"))
If someone is kind and nice then they chase the lion.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "chases" "lion" "+"))
If someone chases the squirrel and the squirrel sees the bald eagle then the squirrel is nice.
((("someone" "chases" "squirrel" "+") ("squirrel" "sees" "bald eagle" "+")) -> ("squirrel" "is" "nice" "+"))
If someone sees the bald eagle then they see the squirrel.
((("someone" "sees" "bald eagle" "+")) -> ("someone" "sees" "squirrel" "+"))
If the bald eagle sees the squirrel and the squirrel eats the cow then the cow is kind.
((("bald eagle" "sees" "squirrel" "+") ("squirrel" "eats" "cow" "+")) -> ("cow" "is" "kind" "+"))
If someone chases the squirrel and the squirrel eats the lion then they see the lion.
((("someone" "chases" "squirrel" "+") ("squirrel" "eats" "lion" "+")) -> ("someone" "sees" "lion" "+"))
If the squirrel chases the lion and the lion eats the cow then the lion sees the bald eagle.
((("squirrel" "chases" "lion" "+") ("lion" "eats" "cow" "+")) -> ("lion" "sees" "bald eagle" "+"))
If someone is kind and they see the lion then they chase the squirrel.
((("someone" "is" "kind" "+") ("someone" "sees" "lion" "+")) -> ("someone" "chases" "squirrel" "+"))
The lion is nice.
True
1
proof
[(triple5)]
("lion" "is" "nice" "+")
triple5
The cow does not see the bald eagle.
False
1
inv-proof
[(triple4)]
("cow" "sees" "bald eagle" "-")
triple4
The squirrel sees the squirrel.
True
2
proof
[(((triple9) -> rule4))]
("squirrel" "sees" "squirrel" "+")
((triple9) -> (rule4 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel does not chase the squirrel.
False
3
inv-proof
[(((triple8 triple10) -> rule8))]
("squirrel" "chases" "squirrel" "-")
((triple8 triple10) -> (rule8 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is nice.
True
5
proof
[(((((triple8 triple10) -> rule8) triple9) -> rule3))]
("squirrel" "is" "nice" "+")
((((triple8 triple10) -> (rule8 % int2)) triple9) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel is not nice.
False
5
inv-proof
[(((((triple8 triple10) -> rule8) triple9) -> rule3))]
("squirrel" "is" "nice" "-")
((((triple8 triple10) -> (rule8 % int2)) triple9) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel chases the lion.
True
7
proof
[(((triple8 ((((triple8 triple10) -> rule8) triple9) -> rule3)) -> rule2))]
("squirrel" "chases" "lion" "+")
((triple8 ((((triple8 triple10) -> (rule8 % int3)) triple9) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The squirrel does not chase the lion.
False
7
inv-proof
[(((triple8 ((((triple8 triple10) -> rule8) triple9) -> rule3)) -> rule2))]
("squirrel" "chases" "lion" "-")
((triple8 ((((triple8 triple10) -> (rule8 % int3)) triple9) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The lion does not see the lion.
Unknown
inv-rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "sees" "lion" "-")
The bald eagle sees the lion.
Unknown
rconc
[@1: The bald eagle sees the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "sees" "lion" "+")
The cow is not kind.
Unknown
inv-rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "kind" "-")
The bald eagle sees the squirrel.
Unknown
rconc
[@1: The bald eagle sees the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "sees" "squirrel" "+")
The bald eagle is not nice.
Unknown
inv-random
[@0: The bald eagle is nice.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "nice" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The cow eats the bald eagle.
Unknown
random
[@0: The cow eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "bald eagle" "+")
@0: The bald eagle is red.[(triple1)] The bald eagle sees the cow.[(triple2)] The cow is nice.[(triple3)] The cow sees the bald eagle.[(triple4)] The lion is nice.[(triple5)] The lion is red.[(triple6)] The lion sees the squirrel.[(triple7)] The squirrel is kind.[(triple8)] The squirrel sees the bald eagle.[(triple9)] The squirrel sees the lion.[(triple10)] @1: The cow sees the squirrel.[(((triple4) -> rule4))] The squirrel chases the squirrel.[(((triple8 triple10) -> rule8))] The squirrel sees the squirrel.[(((triple9) -> rule4))] @2: The squirrel is nice.[(((((triple8 triple10) -> rule8) triple9) -> rule3))] @3: The squirrel chases the lion.[(((triple8 ((((triple8 triple10) -> rule8) triple9) -> rule3)) -> rule2))]
The bald eagle is red.
("bald eagle" "is" "red" "+")
triple1
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
triple4
The lion is nice.
("lion" "is" "nice" "+")
triple5
The lion is red.
("lion" "is" "red" "+")
triple6
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple7
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple8
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
triple9
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple10
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
((triple4) -> (rule4 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple8 triple10) -> (rule8 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple9) -> (rule4 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((((triple8 triple10) -> (rule8 % int2)) triple9) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
((triple8 ((((triple8 triple10) -> (rule8 % int3)) triple9) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3