The bald eagle visits the squirrel. The squirrel chases the bald eagle. The tiger sees the squirrel. If something chases the bald eagle then it chases the tiger. If the squirrel chases the tiger and the tiger sees the squirrel then the tiger chases the bald eagle. If something is nice then it chases the squirrel.
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
The squirrel chases the bald eagle.
("squirrel" "chases" "bald eagle" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If something chases the bald eagle then it chases the tiger.
((("something" "chases" "bald eagle" "+")) -> ("something" "chases" "tiger" "+"))
If the squirrel chases the tiger and the tiger sees the squirrel then the tiger chases the bald eagle.
((("squirrel" "chases" "tiger" "+") ("tiger" "sees" "squirrel" "+")) -> ("tiger" "chases" "bald eagle" "+"))
If something is nice then it chases the squirrel.
((("something" "is" "nice" "+")) -> ("something" "chases" "squirrel" "+"))
The squirrel chases the bald eagle.
True
1
proof
[(triple2)]
("squirrel" "chases" "bald eagle" "+")
triple2
The bald eagle does not visit the squirrel.
False
1
inv-proof
[(triple1)]
("bald eagle" "visits" "squirrel" "-")
triple1
The squirrel chases the tiger.
True
2
proof
[(((triple2) -> rule1))]
("squirrel" "chases" "tiger" "+")
((triple2) -> (rule1 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The squirrel does not chase the tiger.
False
2
inv-proof
[(((triple2) -> rule1))]
("squirrel" "chases" "tiger" "-")
((triple2) -> (rule1 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The bald eagle does not chase the tiger.
Unknown
inv-rconc
[@1: The bald eagle chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "chases" "tiger" "-")
The squirrel chases the squirrel.
Unknown
rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "chases" "squirrel" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The squirrel visits the bald eagle.
Unknown
random
[@0: The squirrel visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "bald eagle" "+")
@0: The bald eagle visits the squirrel.[(triple1)] The squirrel chases the bald eagle.[(triple2)] The tiger sees the squirrel.[(triple3)] @1: The squirrel chases the tiger.[(((triple2) -> rule1))] @2: The tiger chases the bald eagle.[(((((triple2) -> rule1) triple3) -> rule2))] @3: The tiger chases the tiger.[(((((((triple2) -> rule1) triple3) -> rule2)) -> rule1))]
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
triple1
The squirrel chases the bald eagle.
("squirrel" "chases" "bald eagle" "+")
triple2
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple3
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
((triple2) -> (rule1 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The tiger chases the bald eagle.
("tiger" "chases" "bald eagle" "+")
((((triple2) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The tiger chases the bald eagle.
("tiger" "chases" "bald eagle" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((((((triple2) -> (rule1 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger chases the bald eagle.
("tiger" "chases" "bald eagle" "+")
int2
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int3