The cow is big. The cow likes the mouse. The cow needs the mouse. The cow visits the mouse. The mouse likes the cow. The mouse needs the cow. The mouse visits the cow. If someone likes the cow and the cow visits the mouse then the mouse needs the cow. If the cow likes the mouse and the mouse visits the cow then the mouse needs the cow. If someone is big and they like the cow then they visit the cow. If someone likes the cow then the cow likes the mouse. Green people are nice. If someone likes the cow then the cow is green.
The cow is big.
("cow" "is" "big" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If someone likes the cow and the cow visits the mouse then the mouse needs the cow.
((("someone" "likes" "cow" "+") ("cow" "visits" "mouse" "+")) -> ("mouse" "needs" "cow" "+"))
If the cow likes the mouse and the mouse visits the cow then the mouse needs the cow.
((("cow" "likes" "mouse" "+") ("mouse" "visits" "cow" "+")) -> ("mouse" "needs" "cow" "+"))
If someone is big and they like the cow then they visit the cow.
((("someone" "is" "big" "+") ("someone" "likes" "cow" "+")) -> ("someone" "visits" "cow" "+"))
If someone likes the cow then the cow likes the mouse.
((("someone" "likes" "cow" "+")) -> ("cow" "likes" "mouse" "+"))
Green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone likes the cow then the cow is green.
((("someone" "likes" "cow" "+")) -> ("cow" "is" "green" "+"))
The cow is big.
True
1
proof
[(triple1)]
("cow" "is" "big" "+")
triple1
The mouse does not need the cow.
False
1
inv-proof
[(triple6 OR ((triple2 triple7) -> rule2) OR ((triple5 triple4) -> rule1) OR ((((triple5) -> rule4) triple7) -> rule2))]
("mouse" "needs" "cow" "-")
triple6
((triple2 triple7) -> (rule2 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
((triple5 triple4) -> (rule1 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
((((triple5) -> (rule4 % int2)) triple7) -> (rule2 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow is green.
True
2
proof
[(((triple5) -> rule6))]
("cow" "is" "green" "+")
((triple5) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is not green.
False
2
inv-proof
[(((triple5) -> rule6))]
("cow" "is" "green" "-")
((triple5) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is nice.
True
3
proof
[(((((triple5) -> rule6)) -> rule5))]
("cow" "is" "nice" "+")
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not nice.
False
3
inv-proof
[(((((triple5) -> rule6)) -> rule5))]
("cow" "is" "nice" "-")
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The mouse is not nice.
Unknown
inv-rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "nice" "-")
The cow visits the cow.
Unknown
rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "visits" "cow" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow is big.[(triple1)] The cow likes the mouse.[(triple2 OR ((triple5) -> rule4))] The cow needs the mouse.[(triple3)] The cow visits the mouse.[(triple4)] The mouse likes the cow.[(triple5)] The mouse needs the cow.[(triple6 OR ((triple2 triple7) -> rule2) OR ((triple5 triple4) -> rule1) OR ((((triple5) -> rule4) triple7) -> rule2))] The mouse visits the cow.[(triple7)] @1: The cow is green.[(((triple5) -> rule6))] @2: The cow is nice.[(((((triple5) -> rule6)) -> rule5))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple2
((triple5) -> (rule4 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple3
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple4
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple5
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple6
((triple2 triple7) -> (rule2 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
((triple5 triple4) -> (rule1 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
((((triple5) -> (rule4 % int2)) triple7) -> (rule2 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple7
The cow is green.
("cow" "is" "green" "+")
((triple5) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2