The bald eagle visits the squirrel. The cow likes the bald eagle. The squirrel is blue. The tiger needs the cow. Blue things are green. If something is green then it likes the bald eagle. If something likes the bald eagle then it visits the tiger. If something needs the squirrel and the squirrel likes the cow then it likes the cow. If something is cold and it needs the tiger then the tiger needs the squirrel. If something needs the squirrel then the squirrel likes the cow.
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is green then it likes the bald eagle.
((("something" "is" "green" "+")) -> ("something" "likes" "bald eagle" "+"))
If something likes the bald eagle then it visits the tiger.
((("something" "likes" "bald eagle" "+")) -> ("something" "visits" "tiger" "+"))
If something needs the squirrel and the squirrel likes the cow then it likes the cow.
((("something" "needs" "squirrel" "+") ("squirrel" "likes" "cow" "+")) -> ("something" "likes" "cow" "+"))
If something is cold and it needs the tiger then the tiger needs the squirrel.
((("something" "is" "cold" "+") ("something" "needs" "tiger" "+")) -> ("tiger" "needs" "squirrel" "+"))
If something needs the squirrel then the squirrel likes the cow.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "likes" "cow" "+"))
The tiger needs the cow.
True
1
proof
[(triple4)]
("tiger" "needs" "cow" "+")
triple4
The squirrel is not blue.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "blue" "-")
triple3
The squirrel is green.
True
2
proof
[(((triple3) -> rule1))]
("squirrel" "is" "green" "+")
((triple3) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The cow does not visit the tiger.
False
2
inv-proof
[(((triple2) -> rule3))]
("cow" "visits" "tiger" "-")
((triple2) -> (rule3 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The squirrel likes the bald eagle.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("squirrel" "likes" "bald eagle" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel does not like the bald eagle.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("squirrel" "likes" "bald eagle" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel visits the tiger.
True
4
proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
("squirrel" "visits" "tiger" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The squirrel does not visit the tiger.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
("squirrel" "visits" "tiger" "-")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The bald eagle is not green.
Unknown
inv-rconc
[@1: The bald eagle is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "is" "green" "-")
The bald eagle likes the cow.
Unknown
rconc
[@1: The bald eagle likes the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "likes" "cow" "+")
The tiger does not visit the tiger.
Unknown
inv-rconc
[@3: The tiger visits the tiger.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule1 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The squirrel likes the cow.
Unknown
rconc
[@2: The squirrel likes the cow.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("squirrel" "likes" "cow" "+")
The tiger does not need the bald eagle.
Unknown
inv-random
[@0: The tiger needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "bald eagle" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
The bald eagle does not need the bald eagle.
Unknown
inv-random
[@0: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "bald eagle" "-")
The bald eagle visits the cow.
Unknown
random
[@0: The bald eagle visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "cow" "+")
@0: The bald eagle visits the squirrel.[(triple1)] The cow likes the bald eagle.[(triple2)] The squirrel is blue.[(triple3)] The tiger needs the cow.[(triple4)] @1: The cow visits the tiger.[(((triple2) -> rule3))] The squirrel is green.[(((triple3) -> rule1))] @2: The squirrel likes the bald eagle.[(((((triple3) -> rule1)) -> rule2))] @3: The squirrel visits the tiger.[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
triple1
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
triple2
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple3
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple4
The cow visits the tiger.
("cow" "visits" "tiger" "+")
((triple2) -> (rule3 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
((triple3) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3