The bald eagle needs the mouse. The cat visits the mouse. The mouse does not chase the cat. The tiger needs the mouse. If something needs the mouse then it visits the cat. If something visits the cat then the cat is red.
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If something needs the mouse then it visits the cat.
((("something" "needs" "mouse" "+")) -> ("something" "visits" "cat" "+"))
If something visits the cat then the cat is red.
((("something" "visits" "cat" "+")) -> ("cat" "is" "red" "+"))
The tiger needs the mouse.
True
1
proof
[(triple4)]
("tiger" "needs" "mouse" "+")
triple4
The mouse chases the cat.
False
1
inv-proof
[(triple3)]
("mouse" "chases" "cat" "+")
triple3
The tiger visits the cat.
True
2
proof
[(((triple4) -> rule1))]
("tiger" "visits" "cat" "+")
((triple4) -> (rule1 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The tiger does not visit the cat.
False
2
inv-proof
[(((triple4) -> rule1))]
("tiger" "visits" "cat" "-")
((triple4) -> (rule1 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The cat is red.
True
3
proof
[(((((triple1) -> rule1)) -> rule2) OR ((((triple4) -> rule1)) -> rule2))]
("cat" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The cat is not red.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2) OR ((((triple4) -> rule1)) -> rule2))]
("cat" "is" "red" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The mouse does not visit the cat.
Unknown
inv-rconc
[@1: The mouse visits the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "cat" "-")
The cat visits the cat.
Unknown
rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "visits" "cat" "+")
The cat does not need the bald eagle.
Unknown
inv-random
[@0: The cat needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "bald eagle" "-")
The mouse visits the bald eagle.
Unknown
random
[@0: The mouse visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bald eagle" "+")
The cat does not visit the tiger.
Unknown
inv-random
[@0: The cat visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "tiger" "-")
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 needs the mouse.[(triple1)] The cat visits the mouse.[(triple2)] The mouse does not chase the cat.[(triple3)] The tiger needs the mouse.[(triple4)] @1: The bald eagle visits the cat.[(((triple1) -> rule1))] The tiger visits the cat.[(((triple4) -> rule1))] @2: The cat is red.[(((((triple1) -> rule1)) -> rule2) OR ((((triple4) -> rule1)) -> rule2))]
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
triple1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple2
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
triple3
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple4
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
((triple1) -> (rule1 % int1))
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
((triple4) -> (rule1 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2