The cat likes the cow. The cow needs the cat. The mouse is big. If something needs the cow and the cow needs the mouse then the mouse does not need the cow. If something needs the cat then it does not like the cat. If something is young and it does not need the mouse then it visits the cat. If something needs the mouse and the mouse does not need the cow then the mouse likes the cow. Green things are big. If something likes the cow then the cow is green.
The cat likes the cow.
("cat" "likes" "cow" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The mouse is big.
("mouse" "is" "big" "+")
If something needs the cow and the cow needs the mouse then the mouse does not need the cow.
((("something" "needs" "cow" "+") ("cow" "needs" "mouse" "+")) -> ("mouse" "needs" "cow" "-"))
If something needs the cat then it does not like the cat.
((("something" "needs" "cat" "+")) -> ("something" "likes" "cat" "-"))
If something is young and it does not need the mouse then it visits the cat.
((("something" "is" "young" "+") ("something" "needs" "mouse" "~")) -> ("something" "visits" "cat" "+"))
If something needs the mouse and the mouse does not need the cow then the mouse likes the cow.
((("something" "needs" "mouse" "+") ("mouse" "needs" "cow" "~")) -> ("mouse" "likes" "cow" "+"))
Green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something likes the cow then the cow is green.
((("something" "likes" "cow" "+")) -> ("cow" "is" "green" "+"))
The cow needs the cat.
True
1
proof
[(triple2)]
("cow" "needs" "cat" "+")
triple2
The mouse is not big.
False
1
inv-proof
[(triple3)]
("mouse" "is" "big" "-")
triple3
The cow does not like the cat.
True
2
proof
[(((triple2) -> rule2))]
("cow" "likes" "cat" "-")
((triple2) -> (rule2 % int1))
The cow does not like the cat.
("cow" "likes" "cat" "-")
int1
The cow likes the cat.
False
2
inv-proof
[(((triple2) -> rule2))]
("cow" "likes" "cat" "+")
((triple2) -> (rule2 % int1))
The cow does not like the cat.
("cow" "likes" "cat" "-")
int1
The cow is big.
True
3
proof
[(((((triple1) -> rule6)) -> rule5))]
("cow" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not big.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule5))]
("cow" "is" "big" "-")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The mouse does not visit the cat.
Unknown
inv-rconc
[@1: The mouse visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "visits" "cat" "-")
The cat is big.
Unknown
rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "big" "+")
The cow does not visit the cat.
Unknown
inv-rconc
[@1: The cow visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "visits" "cat" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The cat likes the cow.[(triple1)] The cow needs the cat.[(triple2)] The mouse is big.[(triple3)] @1: The cow does not like the cat.[(((triple2) -> rule2))] The cow is green.[(((triple1) -> rule6))] @2: The cow is big.[(((((triple1) -> rule6)) -> rule5))]
The cat likes the cow.
("cat" "likes" "cow" "+")
triple1
The cow needs the cat.
("cow" "needs" "cat" "+")
triple2
The mouse is big.
("mouse" "is" "big" "+")
triple3
The cow does not like the cat.
("cow" "likes" "cat" "-")
((triple2) -> (rule2 % int1))
The cow does not like the cat.
("cow" "likes" "cat" "-")
int1
The cow is green.
("cow" "is" "green" "+")
((triple1) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is big.
("cow" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2