The cat does not see the cow. The cat sees the lion. The cat visits the mouse. The cow is cold. The cow is green. The cow is nice. The lion needs the cow. The mouse is cold. The mouse is green. The mouse is kind. The mouse is not nice. The mouse needs the cat. The mouse needs the cow. The mouse sees the cow. The mouse sees the lion. The mouse visits the lion. If something needs the cow and it is not green then the cow sees the cat. If something needs the lion then the lion visits the mouse. If the lion needs the mouse then the lion is kind. Young, kind things are nice. If something sees the lion then it needs the lion. If something is green and it does not see the mouse then it is young. If something visits the cow then it does not visit the cat. If something is cold then it needs the mouse.
The cat does not see the cow.
("cat" "sees" "cow" "-")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is not nice.
("mouse" "is" "nice" "-")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If something needs the cow and it is not green then the cow sees the cat.
((("something" "needs" "cow" "+") ("something" "is" "green" "~")) -> ("cow" "sees" "cat" "+"))
If something needs the lion then the lion visits the mouse.
((("something" "needs" "lion" "+")) -> ("lion" "visits" "mouse" "+"))
If the lion needs the mouse then the lion is kind.
((("lion" "needs" "mouse" "+")) -> ("lion" "is" "kind" "+"))
Young, kind things are nice.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something sees the lion then it needs the lion.
((("something" "sees" "lion" "+")) -> ("something" "needs" "lion" "+"))
If something is green and it does not see the mouse then it is young.
((("something" "is" "green" "+") ("something" "sees" "mouse" "~")) -> ("something" "is" "young" "+"))
If something visits the cow then it does not visit the cat.
((("something" "visits" "cow" "+")) -> ("something" "visits" "cat" "-"))
If something is cold then it needs the mouse.
((("something" "is" "cold" "+")) -> ("something" "needs" "mouse" "+"))
The mouse sees the cow.
True
1
proof
[(triple14)]
("mouse" "sees" "cow" "+")
triple14
The cat does not visit the mouse.
False
1
inv-proof
[(triple3)]
("cat" "visits" "mouse" "-")
triple3
The mouse needs the mouse.
True
2
proof
[(((triple8) -> rule8))]
("mouse" "needs" "mouse" "+")
((triple8) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The cow does not need the mouse.
False
2
inv-proof
[(((triple4) -> rule8))]
("cow" "needs" "mouse" "-")
((triple4) -> (rule8 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The lion visits the mouse.
True
3
proof
[(((((triple15) -> rule5)) -> rule2) OR ((((triple2) -> rule5)) -> rule2))]
("lion" "visits" "mouse" "+")
((((triple15) -> (rule5 % int2))) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The lion does not visit the mouse.
False
3
inv-proof
[(((((triple15) -> rule5)) -> rule2) OR ((((triple2) -> rule5)) -> rule2))]
("lion" "visits" "mouse" "-")
((((triple15) -> (rule5 % int2))) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "young" "-")
The cow sees the cat.
Unknown
rconc
[@1: The cow sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "cat" "+")
The lion does not need the mouse.
Unknown
inv-rconc
[@1: The lion needs the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "needs" "mouse" "-")
The lion visits the cow.
Unknown
random
[@0: The lion visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cow" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The cat does not see the cow.[(triple1)] The cat sees the lion.[(triple2)] The cat visits the mouse.[(triple3)] The cow is cold.[(triple4)] The cow is green.[(triple5)] The cow is nice.[(triple6)] The lion needs the cow.[(triple7)] The mouse is cold.[(triple8)] The mouse is green.[(triple9)] The mouse is kind.[(triple10)] The mouse is not nice.[(triple11)] The mouse needs the cat.[(triple12)] The mouse needs the cow.[(triple13)] The mouse sees the cow.[(triple14)] The mouse sees the lion.[(triple15)] The mouse visits the lion.[(triple16)] @1: The cat needs the lion.[(((triple2) -> rule5))] The cow needs the mouse.[(((triple4) -> rule8))] The mouse needs the lion.[(((triple15) -> rule5))] The mouse needs the mouse.[(((triple8) -> rule8))] @2: The lion visits the mouse.[(((((triple15) -> rule5)) -> rule2) OR ((((triple2) -> rule5)) -> rule2))]
The cat does not see the cow.
("cat" "sees" "cow" "-")
triple1
The cat sees the lion.
("cat" "sees" "lion" "+")
triple2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple3
The cow is cold.
("cow" "is" "cold" "+")
triple4
The cow is green.
("cow" "is" "green" "+")
triple5
The cow is nice.
("cow" "is" "nice" "+")
triple6
The lion needs the cow.
("lion" "needs" "cow" "+")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
triple8
The mouse is green.
("mouse" "is" "green" "+")
triple9
The mouse is kind.
("mouse" "is" "kind" "+")
triple10
The mouse is not nice.
("mouse" "is" "nice" "-")
triple11
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple12
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple13
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple14
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple15
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple16
The cat needs the lion.
("cat" "needs" "lion" "+")
((triple2) -> (rule5 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((triple4) -> (rule8 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
((triple15) -> (rule5 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple8) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
((((triple15) -> (rule5 % int2))) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2