The bald eagle likes the squirrel. The mouse likes the tiger. The squirrel chases the mouse. The squirrel likes the tiger. The tiger is not blue. The tiger likes the mouse. The tiger likes the squirrel. If something is red and it likes the mouse then the mouse does not like the squirrel. If something likes the bald eagle then it likes the mouse. If the mouse likes the squirrel then the squirrel chases the bald eagle. If the tiger does not chase the mouse then the mouse is not round. If something likes the bald eagle then it chases the tiger. If something likes the squirrel then the squirrel likes the bald eagle. If the squirrel needs the bald eagle then the squirrel is not rough. If something is nice and it does not like the bald eagle then the bald eagle is rough.
The bald eagle likes the squirrel.
("bald eagle" "likes" "squirrel" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The tiger is not blue.
("tiger" "is" "blue" "-")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
If something is red and it likes the mouse then the mouse does not like the squirrel.
((("something" "is" "red" "+") ("something" "likes" "mouse" "+")) -> ("mouse" "likes" "squirrel" "-"))
If something likes the bald eagle then it likes the mouse.
((("something" "likes" "bald eagle" "+")) -> ("something" "likes" "mouse" "+"))
If the mouse likes the squirrel then the squirrel chases the bald eagle.
((("mouse" "likes" "squirrel" "+")) -> ("squirrel" "chases" "bald eagle" "+"))
If the tiger does not chase the mouse then the mouse is not round.
((("tiger" "chases" "mouse" "~")) -> ("mouse" "is" "round" "-"))
If something likes the bald eagle then it chases the tiger.
((("something" "likes" "bald eagle" "+")) -> ("something" "chases" "tiger" "+"))
If something likes the squirrel then the squirrel likes the bald eagle.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "likes" "bald eagle" "+"))
If the squirrel needs the bald eagle then the squirrel is not rough.
((("squirrel" "needs" "bald eagle" "+")) -> ("squirrel" "is" "rough" "-"))
If something is nice and it does not like the bald eagle then the bald eagle is rough.
((("something" "is" "nice" "+") ("something" "likes" "bald eagle" "~")) -> ("bald eagle" "is" "rough" "+"))
The bald eagle likes the squirrel.
True
1
proof
[(triple1)]
("bald eagle" "likes" "squirrel" "+")
triple1
The mouse does not like the tiger.
False
1
inv-proof
[(triple2)]
("mouse" "likes" "tiger" "-")
triple2
The squirrel likes the bald eagle.
True
2
proof
[(((triple1) -> rule6) OR ((triple7) -> rule6))]
("squirrel" "likes" "bald eagle" "+")
((triple1) -> (rule6 % int1))
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int1
((triple7) -> (rule6 % int1))
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int1
The squirrel does not like the bald eagle.
False
2
inv-proof
[(((triple1) -> rule6) OR ((triple7) -> rule6))]
("squirrel" "likes" "bald eagle" "-")
((triple1) -> (rule6 % int1))
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int1
((triple7) -> (rule6 % int1))
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int1
The squirrel likes the mouse.
True
3
proof
[(((((triple1) -> rule6)) -> rule2) OR ((((triple7) -> rule6)) -> rule2))]
("squirrel" "likes" "mouse" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int2
((((triple7) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int2
The squirrel does not chase the tiger.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule5) OR ((((triple7) -> rule6)) -> rule5))]
("squirrel" "chases" "tiger" "-")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int2
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int2
The squirrel does not chase the bald eagle.
Unknown
inv-rconc
[@1: The squirrel chases the bald eagle.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "chases" "bald eagle" "-")
The mouse chases the tiger.
Unknown
rconc
[@1: The mouse chases the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "chases" "tiger" "+")
The bald eagle does not like the mouse.
Unknown
inv-rconc
[@1: The bald eagle likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "likes" "mouse" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
The tiger does not chase the squirrel.
Unknown
inv-random
[@0: The tiger chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "squirrel" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
@0: The bald eagle likes the squirrel.[(triple1)] The mouse likes the tiger.[(triple2)] The squirrel chases the mouse.[(triple3)] The squirrel likes the tiger.[(triple4)] The tiger is not blue.[(triple5)] The tiger likes the mouse.[(triple6)] The tiger likes the squirrel.[(triple7)] @1: The squirrel likes the bald eagle.[(((triple1) -> rule6) OR ((triple7) -> rule6))] @2: The squirrel chases the tiger.[(((((triple1) -> rule6)) -> rule5) OR ((((triple7) -> rule6)) -> rule5))] The squirrel likes the mouse.[(((((triple1) -> rule6)) -> rule2) OR ((((triple7) -> rule6)) -> rule2))]
The bald eagle likes the squirrel.
("bald eagle" "likes" "squirrel" "+")
triple1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple2
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple3
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple4
The tiger is not blue.
("tiger" "is" "blue" "-")
triple5
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple6
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple7
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
((triple1) -> (rule6 % int1))
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int1
((triple7) -> (rule6 % int1))
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int2
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int2
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int2
((((triple7) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int2