The cow eats the mouse. The cow is not big. The cow is green. The cow is red. The mouse eats the cow. The mouse is big. The mouse is not blue. The mouse is round. The mouse sees the cow. The mouse does not visit the cow. If something eats the cow and it is round then it visits the mouse. If the mouse sees the cow then the cow is green. If something is round and it eats the mouse then it sees the mouse. If something visits the mouse then it sees the mouse. If something visits the mouse and it is not round then it is not red. If something sees the cow and the cow eats the mouse then the cow sees the mouse.
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow is not big.
("cow" "is" "big" "-")
The cow is green.
("cow" "is" "green" "+")
The cow is red.
("cow" "is" "red" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is not blue.
("mouse" "is" "blue" "-")
The mouse is round.
("mouse" "is" "round" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
If something eats the cow and it is round then it visits the mouse.
((("something" "eats" "cow" "+") ("something" "is" "round" "+")) -> ("something" "visits" "mouse" "+"))
If the mouse sees the cow then the cow is green.
((("mouse" "sees" "cow" "+")) -> ("cow" "is" "green" "+"))
If something is round and it eats the mouse then it sees the mouse.
((("something" "is" "round" "+") ("something" "eats" "mouse" "+")) -> ("something" "sees" "mouse" "+"))
If something visits the mouse then it sees the mouse.
((("something" "visits" "mouse" "+")) -> ("something" "sees" "mouse" "+"))
If something visits the mouse and it is not round then it is not red.
((("something" "visits" "mouse" "+") ("something" "is" "round" "~")) -> ("something" "is" "red" "-"))
If something sees the cow and the cow eats the mouse then the cow sees the mouse.
((("something" "sees" "cow" "+") ("cow" "eats" "mouse" "+")) -> ("cow" "sees" "mouse" "+"))
The mouse does not visit the cow.
True
1
proof
[(triple10)]
("mouse" "visits" "cow" "-")
triple10
The mouse is not round.
False
1
inv-proof
[(triple8)]
("mouse" "is" "round" "-")
triple8
The mouse visits the mouse.
True
3
proof
[(((triple5 triple8) -> rule1))]
("mouse" "visits" "mouse" "+")
((triple5 triple8) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The cow does not see the mouse.
False
3
inv-proof
[(((triple9 triple1) -> rule6))]
("cow" "sees" "mouse" "-")
((triple9 triple1) -> (rule6 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The mouse sees the mouse.
True
4
proof
[(((((triple5 triple8) -> rule1)) -> rule4))]
("mouse" "sees" "mouse" "+")
((((triple5 triple8) -> (rule1 % int2))) -> (rule4 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse does not see the mouse.
False
4
inv-proof
[(((((triple5 triple8) -> rule1)) -> rule4))]
("mouse" "sees" "mouse" "-")
((((triple5 triple8) -> (rule1 % int2))) -> (rule4 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The cow does not visit the mouse.
Unknown
inv-rconc
[@1: The cow visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "mouse" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
@0: The cow eats the mouse.[(triple1)] The cow is green.[(triple3 OR ((triple9) -> rule2))] The cow is not big.[(triple2)] The cow is red.[(triple4)] The mouse does not visit the cow.[(triple10)] The mouse eats the cow.[(triple5)] The mouse is big.[(triple6)] The mouse is not blue.[(triple7)] The mouse is round.[(triple8)] The mouse sees the cow.[(triple9)] @1: The cow sees the mouse.[(((triple9 triple1) -> rule6))] The mouse visits the mouse.[(((triple5 triple8) -> rule1))] @2: The mouse sees the mouse.[(((((triple5 triple8) -> rule1)) -> rule4))]
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple3
((triple9) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is not big.
("cow" "is" "big" "-")
triple2
The cow is red.
("cow" "is" "red" "+")
triple4
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
triple10
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple5
The mouse is big.
("mouse" "is" "big" "+")
triple6
The mouse is not blue.
("mouse" "is" "blue" "-")
triple7
The mouse is round.
("mouse" "is" "round" "+")
triple8
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple9
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((triple9 triple1) -> (rule6 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple5 triple8) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple5 triple8) -> (rule1 % int2))) -> (rule4 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2