The bald eagle likes the squirrel. The cat needs the bald eagle. The squirrel needs the tiger. The tiger is cold. If something needs the cat then the cat visits the bald eagle. If something needs the bald eagle then the bald eagle is young. If something is young then it visits the squirrel.
The bald eagle likes the squirrel.
("bald eagle" "likes" "squirrel" "+")
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
If something needs the cat then the cat visits the bald eagle.
((("something" "needs" "cat" "+")) -> ("cat" "visits" "bald eagle" "+"))
If something needs the bald eagle then the bald eagle is young.
((("something" "needs" "bald eagle" "+")) -> ("bald eagle" "is" "young" "+"))
If something is young then it visits the squirrel.
((("something" "is" "young" "+")) -> ("something" "visits" "squirrel" "+"))
The squirrel needs the tiger.
True
1
proof
[(triple3)]
("squirrel" "needs" "tiger" "+")
triple3
The tiger is not cold.
False
1
inv-proof
[(triple4)]
("tiger" "is" "cold" "-")
triple4
The bald eagle is young.
True
2
proof
[(((triple2) -> rule2))]
("bald eagle" "is" "young" "+")
((triple2) -> (rule2 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle is not young.
False
2
inv-proof
[(((triple2) -> rule2))]
("bald eagle" "is" "young" "-")
((triple2) -> (rule2 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle visits the squirrel.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("bald eagle" "visits" "squirrel" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle does not visit the squirrel.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("bald eagle" "visits" "squirrel" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The tiger visits the squirrel.
Unknown
rconc
[@1: The tiger visits the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "squirrel" "+")
The cat does not visit the squirrel.
Unknown
inv-rconc
[@1: The cat visits the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "visits" "squirrel" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The tiger visits the bald eagle.
Unknown
random
[@0: The tiger visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "bald eagle" "+")
@0: The bald eagle likes the squirrel.[(triple1)] The cat needs the bald eagle.[(triple2)] The squirrel needs the tiger.[(triple3)] The tiger is cold.[(triple4)] @1: The bald eagle is young.[(((triple2) -> rule2))] @2: The bald eagle visits the squirrel.[(((((triple2) -> rule2)) -> rule3))]
The bald eagle likes the squirrel.
("bald eagle" "likes" "squirrel" "+")
triple1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
triple2
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple3
The tiger is cold.
("tiger" "is" "cold" "+")
triple4
The bald eagle is young.
("bald eagle" "is" "young" "+")
((triple2) -> (rule2 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2