The bald eagle needs the bear. The bear does not eat the mouse. The mouse visits the tiger. The tiger is red. If something needs the tiger and it does not eat the mouse then the tiger eats the bear. Young, cold things are rough. If something visits the mouse then the mouse eats the tiger. If the mouse visits the tiger then the tiger visits the mouse. If something eats the mouse and it eats the bear then the bear does not need the tiger. If the tiger eats the bald eagle and the tiger does not need the bald eagle then the bald eagle is not red. If the bald eagle needs the bear and the bald eagle is not cold then the bear does not visit the tiger. If something is nice and it needs the bear then it does not need the tiger.
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
The bear does not eat the mouse.
("bear" "eats" "mouse" "-")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
If something needs the tiger and it does not eat the mouse then the tiger eats the bear.
((("something" "needs" "tiger" "+") ("something" "eats" "mouse" "~")) -> ("tiger" "eats" "bear" "+"))
Young, cold things are rough.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something visits the mouse then the mouse eats the tiger.
((("something" "visits" "mouse" "+")) -> ("mouse" "eats" "tiger" "+"))
If the mouse visits the tiger then the tiger visits the mouse.
((("mouse" "visits" "tiger" "+")) -> ("tiger" "visits" "mouse" "+"))
If something eats the mouse and it eats the bear then the bear does not need the tiger.
((("something" "eats" "mouse" "+") ("something" "eats" "bear" "+")) -> ("bear" "needs" "tiger" "-"))
If the tiger eats the bald eagle and the tiger does not need the bald eagle then the bald eagle is not red.
((("tiger" "eats" "bald eagle" "+") ("tiger" "needs" "bald eagle" "~")) -> ("bald eagle" "is" "red" "-"))
If the bald eagle needs the bear and the bald eagle is not cold then the bear does not visit the tiger.
((("bald eagle" "needs" "bear" "+") ("bald eagle" "is" "cold" "~")) -> ("bear" "visits" "tiger" "-"))
If something is nice and it needs the bear then it does not need the tiger.
((("something" "is" "nice" "+") ("something" "needs" "bear" "+")) -> ("something" "needs" "tiger" "-"))
The tiger is red.
True
1
proof
[(triple4)]
("tiger" "is" "red" "+")
triple4
The tiger is not red.
False
1
inv-proof
[(triple4)]
("tiger" "is" "red" "-")
triple4
The tiger visits the mouse.
True
2
proof
[(((triple3) -> rule4))]
("tiger" "visits" "mouse" "+")
((triple3) -> (rule4 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger does not visit the mouse.
False
2
inv-proof
[(((triple3) -> rule4))]
("tiger" "visits" "mouse" "-")
((triple3) -> (rule4 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse eats the tiger.
True
3
proof
[(((((triple3) -> rule4)) -> rule3))]
("mouse" "eats" "tiger" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The mouse does not eat the tiger.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule3))]
("mouse" "eats" "tiger" "-")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The tiger does not eat the bear.
Unknown
inv-rconc
[@1: The tiger eats the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "eats" "bear" "-")
The bald eagle is rough.
Unknown
rconc
[@1: The bald eagle is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "rough" "+")
The tiger is not rough.
Unknown
inv-rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "rough" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The mouse does not eat the bald eagle.
Unknown
inv-random
[@0: The mouse eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "bald eagle" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
@0: The bald eagle needs the bear.[(triple1)] The bear does not eat the mouse.[(triple2)] The mouse visits the tiger.[(triple3)] The tiger is red.[(triple4)] @1: The tiger visits the mouse.[(((triple3) -> rule4))] @2: The mouse eats the tiger.[(((((triple3) -> rule4)) -> rule3))]
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
triple1
The bear does not eat the mouse.
("bear" "eats" "mouse" "-")
triple2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple3
The tiger is red.
("tiger" "is" "red" "+")
triple4
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
((triple3) -> (rule4 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2