The bald eagle needs the dog. The dog sees the squirrel. The squirrel sees the tiger. The tiger visits the squirrel. If something visits the bald eagle then it visits the tiger. If something sees the tiger then it visits the bald eagle. If something needs the tiger and it is nice then it is not big. If something sees the bald eagle and the bald eagle is red then it needs the tiger. If the dog does not need the squirrel then the squirrel is nice. If something sees the tiger and it does not see the squirrel then the squirrel needs the tiger.
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If something visits the bald eagle then it visits the tiger.
((("something" "visits" "bald eagle" "+")) -> ("something" "visits" "tiger" "+"))
If something sees the tiger then it visits the bald eagle.
((("something" "sees" "tiger" "+")) -> ("something" "visits" "bald eagle" "+"))
If something needs the tiger and it is nice then it is not big.
((("something" "needs" "tiger" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "-"))
If something sees the bald eagle and the bald eagle is red then it needs the tiger.
((("something" "sees" "bald eagle" "+") ("bald eagle" "is" "red" "+")) -> ("something" "needs" "tiger" "+"))
If the dog does not need the squirrel then the squirrel is nice.
((("dog" "needs" "squirrel" "~")) -> ("squirrel" "is" "nice" "+"))
If something sees the tiger and it does not see the squirrel then the squirrel needs the tiger.
((("something" "sees" "tiger" "+") ("something" "sees" "squirrel" "~")) -> ("squirrel" "needs" "tiger" "+"))
The squirrel sees the tiger.
True
1
proof
[(triple3)]
("squirrel" "sees" "tiger" "+")
triple3
The tiger does not visit the squirrel.
False
1
inv-proof
[(triple4)]
("tiger" "visits" "squirrel" "-")
triple4
The squirrel visits the bald eagle.
True
2
proof
[(((triple3) -> rule2))]
("squirrel" "visits" "bald eagle" "+")
((triple3) -> (rule2 % int1))
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
int1
The squirrel does not visit the bald eagle.
False
2
inv-proof
[(((triple3) -> rule2))]
("squirrel" "visits" "bald eagle" "-")
((triple3) -> (rule2 % int1))
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
int1
The squirrel does not need the tiger.
Unknown
inv-rconc
[@1: The squirrel needs the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "needs" "tiger" "-")
The bald eagle visits the bald eagle.
Unknown
rconc
[@1: The bald eagle visits the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "visits" "bald eagle" "+")
The bald eagle is not cold.
Unknown
inv-random
[@0: The bald eagle is cold.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "cold" "-")
The bald eagle sees the bald eagle.
Unknown
random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "+")
@0: The bald eagle needs the dog.[(triple1)] The dog sees the squirrel.[(triple2)] The squirrel sees the tiger.[(triple3)] The tiger visits the squirrel.[(triple4)] @1: The squirrel visits the bald eagle.[(((triple3) -> rule2))] @2: The squirrel visits the tiger.[(((((triple3) -> rule2)) -> rule1))]
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
triple1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple2
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple3
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple4
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
((triple3) -> (rule2 % int1))
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
int2