The cat is blue. The mouse needs the cat. The mouse sees the cat. If something sees the cat then the cat sees the mouse. If something sees the cat and the cat sees the mouse then the cat visits the mouse. If something visits the mouse then the mouse is round. If something needs the mouse then the mouse needs the cat. If something visits the mouse then it sees the mouse. If the mouse is blue and the mouse is green then the mouse is round. If the cat needs the mouse and the mouse is green then the mouse is nice. If something sees the cat then the cat sees the mouse.
The cat is blue.
("cat" "is" "blue" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If something sees the cat then the cat sees the mouse.
((("something" "sees" "cat" "+")) -> ("cat" "sees" "mouse" "+"))
If something sees the cat and the cat sees the mouse then the cat visits the mouse.
((("something" "sees" "cat" "+") ("cat" "sees" "mouse" "+")) -> ("cat" "visits" "mouse" "+"))
If something visits the mouse then the mouse is round.
((("something" "visits" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If something needs the mouse then the mouse needs the cat.
((("something" "needs" "mouse" "+")) -> ("mouse" "needs" "cat" "+"))
If something visits the mouse then it sees the mouse.
((("something" "visits" "mouse" "+")) -> ("something" "sees" "mouse" "+"))
If the mouse is blue and the mouse is green then the mouse is round.
((("mouse" "is" "blue" "+") ("mouse" "is" "green" "+")) -> ("mouse" "is" "round" "+"))
If the cat needs the mouse and the mouse is green then the mouse is nice.
((("cat" "needs" "mouse" "+") ("mouse" "is" "green" "+")) -> ("mouse" "is" "nice" "+"))
If something sees the cat then the cat sees the mouse.
((("something" "sees" "cat" "+")) -> ("cat" "sees" "mouse" "+"))
The mouse needs the cat.
True
1
proof
[(triple2)]
("mouse" "needs" "cat" "+")
triple2
The cat is not blue.
False
1
inv-proof
[(triple1)]
("cat" "is" "blue" "-")
triple1
The cat sees the mouse.
True
2
proof
[(((triple3) -> rule1) OR ((triple3) -> rule8))]
("cat" "sees" "mouse" "+")
((triple3) -> (rule1 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
((triple3) -> (rule8 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat does not see the mouse.
False
2
inv-proof
[(((triple3) -> rule1) OR ((triple3) -> rule8))]
("cat" "sees" "mouse" "-")
((triple3) -> (rule1 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
((triple3) -> (rule8 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat visits the mouse.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule2) OR ((triple3 ((triple3) -> rule8)) -> rule2))]
("cat" "visits" "mouse" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
((triple3 ((triple3) -> (rule8 % int2))) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The cat does not visit the mouse.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule2) OR ((triple3 ((triple3) -> rule8)) -> rule2))]
("cat" "visits" "mouse" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
((triple3 ((triple3) -> (rule8 % int2))) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The mouse is round.
True
5
proof
[(((((triple3 ((triple3) -> rule1)) -> rule2)) -> rule3) OR ((((triple3 ((triple3) -> rule8)) -> rule2)) -> rule3))]
("mouse" "is" "round" "+")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
((((triple3 ((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The mouse is not round.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule1)) -> rule2)) -> rule3) OR ((((triple3 ((triple3) -> rule8)) -> rule2)) -> rule3))]
("mouse" "is" "round" "-")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
((((triple3 ((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "is" "nice" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat needs the mouse.
Unknown
random
[@0: The cat needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "mouse" "+")
@0: The cat is blue.[(triple1)] The mouse needs the cat.[(triple2)] The mouse sees the cat.[(triple3)] @1: The cat sees the mouse.[(((triple3) -> rule1) OR ((triple3) -> rule8))] @2: The cat visits the mouse.[(((triple3 ((triple3) -> rule1)) -> rule2) OR ((triple3 ((triple3) -> rule8)) -> rule2))] @3: The mouse is round.[(((((triple3 ((triple3) -> rule1)) -> rule2)) -> rule3) OR ((((triple3 ((triple3) -> rule8)) -> rule2)) -> rule3))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple3
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((triple3) -> (rule1 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
((triple3) -> (rule8 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
((triple3 ((triple3) -> (rule8 % int2))) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
((((triple3 ((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3