The bald eagle sees the squirrel. The bald eagle sees the tiger. The lion chases the tiger. The lion sees the tiger. The lion visits the squirrel. The lion visits the tiger. The squirrel chases the bald eagle. The squirrel chases the tiger. The squirrel visits the bald eagle. The tiger sees the squirrel. If something is nice then it visits the bald eagle. If something sees the tiger then the tiger is big.
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The squirrel chases the bald eagle.
("squirrel" "chases" "bald eagle" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If something is nice then it visits the bald eagle.
((("something" "is" "nice" "+")) -> ("something" "visits" "bald eagle" "+"))
If something sees the tiger then the tiger is big.
((("something" "sees" "tiger" "+")) -> ("tiger" "is" "big" "+"))
The lion sees the tiger.
True
1
proof
[(triple4)]
("lion" "sees" "tiger" "+")
triple4
The tiger does not see the squirrel.
False
1
inv-proof
[(triple10)]
("tiger" "sees" "squirrel" "-")
triple10
The tiger is big.
True
2
proof
[(((triple2) -> rule2) OR ((triple4) -> rule2))]
("tiger" "is" "big" "+")
((triple2) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((triple4) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not big.
False
2
inv-proof
[(((triple2) -> rule2) OR ((triple4) -> rule2))]
("tiger" "is" "big" "-")
((triple2) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((triple4) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The lion does not visit the bald eagle.
Unknown
inv-rconc
[@1: The lion visits the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "bald eagle" "-")
The tiger visits the bald eagle.
Unknown
rconc
[@1: The tiger visits the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "bald eagle" "+")
The lion does not see the bald eagle.
Unknown
inv-random
[@0: The lion sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "bald eagle" "-")
The tiger sees the bald eagle.
Unknown
random
[@0: The tiger sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bald eagle" "+")
@0: The bald eagle sees the squirrel.[(triple1)] The bald eagle sees the tiger.[(triple2)] The lion chases the tiger.[(triple3)] The lion sees the tiger.[(triple4)] The lion visits the squirrel.[(triple5)] The lion visits the tiger.[(triple6)] The squirrel chases the bald eagle.[(triple7)] The squirrel chases the tiger.[(triple8)] The squirrel visits the bald eagle.[(triple9)] The tiger sees the squirrel.[(triple10)] @1: The tiger is big.[(((triple2) -> rule2) OR ((triple4) -> rule2))]
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
triple1
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
triple2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple3
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple4
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple5
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple6
The squirrel chases the bald eagle.
("squirrel" "chases" "bald eagle" "+")
triple7
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple8
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
triple9
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple10
The tiger is big.
("tiger" "is" "big" "+")
((triple2) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((triple4) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1