The bear needs the mouse. The cat is young. The mouse is young. If someone is young then they visit the cat. If someone visits the cat then the cat is round.
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The cat is young.
("cat" "is" "young" "+")
The mouse is young.
("mouse" "is" "young" "+")
If someone is young then they visit the cat.
((("someone" "is" "young" "+")) -> ("someone" "visits" "cat" "+"))
If someone visits the cat then the cat is round.
((("someone" "visits" "cat" "+")) -> ("cat" "is" "round" "+"))
The bear needs the mouse.
True
1
proof
[(triple1)]
("bear" "needs" "mouse" "+")
triple1
The mouse is not young.
False
1
inv-proof
[(triple3)]
("mouse" "is" "young" "-")
triple3
The cat visits the cat.
True
2
proof
[(((triple2) -> rule1))]
("cat" "visits" "cat" "+")
((triple2) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat does not visit the cat.
False
2
inv-proof
[(((triple2) -> rule1))]
("cat" "visits" "cat" "-")
((triple2) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is round.
True
3
proof
[(((((triple2) -> rule1)) -> rule2) OR ((((triple3) -> rule1)) -> rule2))]
("cat" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2
The cat is not round.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2) OR ((((triple3) -> rule1)) -> rule2))]
("cat" "is" "round" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2
The bear does not visit the cat.
Unknown
inv-rconc
[@1: The bear visits the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "cat" "-")
The mouse eats the bear.
Unknown
random
[@0: The mouse eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "bear" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The mouse needs the cat.
Unknown
random
[@0: The mouse needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cat" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The bear eats the mouse.
Unknown
random
[@0: The bear eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "mouse" "+")
@0: The bear needs the mouse.[(triple1)] The cat is young.[(triple2)] The mouse is young.[(triple3)] @1: The cat visits the cat.[(((triple2) -> rule1))] The mouse visits the cat.[(((triple3) -> rule1))] @2: The cat is round.[(((((triple2) -> rule1)) -> rule2) OR ((((triple3) -> rule1)) -> rule2))]
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple1
The cat is young.
("cat" "is" "young" "+")
triple2
The mouse is young.
("mouse" "is" "young" "+")
triple3
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple2) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
((triple3) -> (rule1 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2