The cow chases the lion. The cow likes the lion. The lion chases the cow. The lion chases the mouse. The lion is kind. The lion likes the mouse. The lion needs the cow. The mouse chases the cow. The mouse is blue. The mouse is kind. If something chases the cow then it is blue. If something likes the lion and the lion is red then the lion needs the mouse. If something likes the mouse then the mouse needs the lion. If something likes the mouse and it chases the mouse then it likes the cow. If something chases the lion then the lion is blue. If something likes the cow and the cow chases the lion then it is red.
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
If something chases the cow then it is blue.
((("something" "chases" "cow" "+")) -> ("something" "is" "blue" "+"))
If something likes the lion and the lion is red then the lion needs the mouse.
((("something" "likes" "lion" "+") ("lion" "is" "red" "+")) -> ("lion" "needs" "mouse" "+"))
If something likes the mouse then the mouse needs the lion.
((("something" "likes" "mouse" "+")) -> ("mouse" "needs" "lion" "+"))
If something likes the mouse and it chases the mouse then it likes the cow.
((("something" "likes" "mouse" "+") ("something" "chases" "mouse" "+")) -> ("something" "likes" "cow" "+"))
If something chases the lion then the lion is blue.
((("something" "chases" "lion" "+")) -> ("lion" "is" "blue" "+"))
If something likes the cow and the cow chases the lion then it is red.
((("something" "likes" "cow" "+") ("cow" "chases" "lion" "+")) -> ("something" "is" "red" "+"))
The lion chases the cow.
True
1
proof
[(triple3)]
("lion" "chases" "cow" "+")
triple3
The mouse does not chase the cow.
False
1
inv-proof
[(triple8)]
("mouse" "chases" "cow" "-")
triple8
The mouse needs the lion.
True
2
proof
[(((triple6) -> rule3))]
("mouse" "needs" "lion" "+")
((triple6) -> (rule3 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse does not need the lion.
False
2
inv-proof
[(((triple6) -> rule3))]
("mouse" "needs" "lion" "-")
((triple6) -> (rule3 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The lion is red.
True
5
proof
[(((((triple6 triple4) -> rule4) triple1) -> rule6))]
("lion" "is" "red" "+")
((((triple6 triple4) -> (rule4 % int2)) triple1) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The lion is not red.
False
5
inv-proof
[(((((triple6 triple4) -> rule4) triple1) -> rule6))]
("lion" "is" "red" "-")
((((triple6 triple4) -> (rule4 % int2)) triple1) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "likes" "cow" "-")
The mouse likes the cow.
Unknown
rconc
[@1: The mouse likes the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "likes" "cow" "+")
The mouse is not red.
Unknown
inv-rconc
[@2: The mouse is red.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("mouse" "is" "red" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The cow chases the lion.[(triple1)] The cow likes the lion.[(triple2)] The lion chases the cow.[(triple3)] The lion chases the mouse.[(triple4)] The lion is kind.[(triple5)] The lion likes the mouse.[(triple6)] The lion needs the cow.[(triple7)] The mouse chases the cow.[(triple8)] The mouse is blue.[(triple9 OR ((triple8) -> rule1))] The mouse is kind.[(triple10)] @1: The lion is blue.[(((triple1) -> rule5) OR ((triple3) -> rule1))] The lion likes the cow.[(((triple6 triple4) -> rule4))] The mouse needs the lion.[(((triple6) -> rule3))] @2: The lion is red.[(((((triple6 triple4) -> rule4) triple1) -> rule6))] @3: The lion needs the mouse.[(((triple2 ((((triple6 triple4) -> rule4) triple1) -> rule6)) -> rule2))]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
The cow likes the lion.
("cow" "likes" "lion" "+")
triple2
The lion chases the cow.
("lion" "chases" "cow" "+")
triple3
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple4
The lion is kind.
("lion" "is" "kind" "+")
triple5
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple6
The lion needs the cow.
("lion" "needs" "cow" "+")
triple7
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple8
The mouse is blue.
("mouse" "is" "blue" "+")
triple9
((triple8) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
triple10
The lion is blue.
("lion" "is" "blue" "+")
((triple1) -> (rule5 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
((triple3) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
((triple6 triple4) -> (rule4 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
((triple6) -> (rule3 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The lion is red.
("lion" "is" "red" "+")
((((triple6 triple4) -> (rule4 % int2)) triple1) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
((triple2 ((((triple6 triple4) -> (rule4 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion likes the cow.
("lion" "likes" "cow" "+")
int3