The bald eagle is blue. The bald eagle sees the squirrel. The lion chases the squirrel. The lion is cold. The lion visits the squirrel. The rabbit chases the bald eagle. The rabbit visits the squirrel. The squirrel is cold. The squirrel visits the lion. The squirrel visits the rabbit. If something sees the lion then it sees the squirrel. If the rabbit sees the bald eagle and the bald eagle visits the squirrel then the rabbit visits the lion. If something sees the bald eagle and it sees the squirrel then the squirrel is nice. If something is cold then it visits the rabbit. If the lion is round then the lion sees the bald eagle. If something is cold and it visits the rabbit then it sees the lion. If the lion chases the squirrel then the lion sees the rabbit. If the squirrel is kind then the squirrel chases the lion.
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If something sees the lion then it sees the squirrel.
((("something" "sees" "lion" "+")) -> ("something" "sees" "squirrel" "+"))
If the rabbit sees the bald eagle and the bald eagle visits the squirrel then the rabbit visits the lion.
((("rabbit" "sees" "bald eagle" "+") ("bald eagle" "visits" "squirrel" "+")) -> ("rabbit" "visits" "lion" "+"))
If something sees the bald eagle and it sees the squirrel then the squirrel is nice.
((("something" "sees" "bald eagle" "+") ("something" "sees" "squirrel" "+")) -> ("squirrel" "is" "nice" "+"))
If something is cold then it visits the rabbit.
((("something" "is" "cold" "+")) -> ("something" "visits" "rabbit" "+"))
If the lion is round then the lion sees the bald eagle.
((("lion" "is" "round" "+")) -> ("lion" "sees" "bald eagle" "+"))
If something is cold and it visits the rabbit then it sees the lion.
((("something" "is" "cold" "+") ("something" "visits" "rabbit" "+")) -> ("something" "sees" "lion" "+"))
If the lion chases the squirrel then the lion sees the rabbit.
((("lion" "chases" "squirrel" "+")) -> ("lion" "sees" "rabbit" "+"))
If the squirrel is kind then the squirrel chases the lion.
((("squirrel" "is" "kind" "+")) -> ("squirrel" "chases" "lion" "+"))
The squirrel visits the lion.
True
1
proof
[(triple9)]
("squirrel" "visits" "lion" "+")
triple9
The lion does not chase the squirrel.
False
1
inv-proof
[(triple3)]
("lion" "chases" "squirrel" "-")
triple3
The lion sees the rabbit.
True
2
proof
[(((triple3) -> rule7))]
("lion" "sees" "rabbit" "+")
((triple3) -> (rule7 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The lion does not see the rabbit.
False
2
inv-proof
[(((triple3) -> rule7))]
("lion" "sees" "rabbit" "-")
((triple3) -> (rule7 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The lion sees the lion.
True
4
proof
[(((triple4 ((triple4) -> rule4)) -> rule6))]
("lion" "sees" "lion" "+")
((triple4 ((triple4) -> (rule4 % int2))) -> (rule6 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int2
The squirrel does not see the squirrel.
False
4
inv-proof
[(((((triple8 triple10) -> rule6)) -> rule1) OR ((((triple8 ((triple8) -> rule4)) -> rule6)) -> rule1))]
("squirrel" "sees" "squirrel" "-")
((((triple8 triple10) -> (rule6 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
((((triple8 ((triple8) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int3
The lion sees the squirrel.
True
5
proof
[(((((triple4 ((triple4) -> rule4)) -> rule6)) -> rule1))]
("lion" "sees" "squirrel" "+")
((((triple4 ((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int3
The lion does not see the squirrel.
False
5
inv-proof
[(((((triple4 ((triple4) -> rule4)) -> rule6)) -> rule1))]
("lion" "sees" "squirrel" "-")
((((triple4 ((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int3
The lion does not see the bald eagle.
Unknown
inv-rconc
[@1: The lion sees the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "sees" "bald eagle" "-")
The squirrel is nice.
Unknown
rconc
[@2: The squirrel is nice.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("squirrel" "is" "nice" "+")
The squirrel does not chase the lion.
Unknown
inv-rconc
[@1: The squirrel chases the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "chases" "lion" "-")
The rabbit sees the lion.
Unknown
rconc
[@1: The rabbit sees the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "sees" "lion" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The bald eagle visits the bald eagle.
Unknown
random
[@0: The bald eagle visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "bald eagle" "+")
The bald eagle does not see the bald eagle.
Unknown
inv-random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "-")
The rabbit sees the bald eagle.
Unknown
random
[@0: The rabbit sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "bald eagle" "+")
@0: The bald eagle is blue.[(triple1)] The bald eagle sees the squirrel.[(triple2)] The lion chases the squirrel.[(triple3)] The lion is cold.[(triple4)] The lion visits the squirrel.[(triple5)] The rabbit chases the bald eagle.[(triple6)] The rabbit visits the squirrel.[(triple7)] The squirrel is cold.[(triple8)] The squirrel visits the lion.[(triple9)] The squirrel visits the rabbit.[(triple10 OR ((triple8) -> rule4))] @1: The lion sees the rabbit.[(((triple3) -> rule7))] The lion visits the rabbit.[(((triple4) -> rule4))] The squirrel sees the lion.[(((triple8 triple10) -> rule6) OR ((triple8 ((triple8) -> rule4)) -> rule6))] @2: The lion sees the lion.[(((triple4 ((triple4) -> rule4)) -> rule6))] The squirrel sees the squirrel.[(((((triple8 triple10) -> rule6)) -> rule1) OR ((((triple8 ((triple8) -> rule4)) -> rule6)) -> rule1))] @3: The lion sees the squirrel.[(((((triple4 ((triple4) -> rule4)) -> rule6)) -> rule1))]
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
triple1
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
triple2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple3
The lion is cold.
("lion" "is" "cold" "+")
triple4
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple5
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
triple6
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple7
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple8
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple9
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple10
((triple8) -> (rule4 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
((triple3) -> (rule7 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
((triple4) -> (rule4 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
((triple8 triple10) -> (rule6 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
((triple8 ((triple8) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple4 ((triple4) -> (rule4 % int2))) -> (rule6 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((triple8 triple10) -> (rule6 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
((((triple8 ((triple8) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int3
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((((triple4 ((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int3