The cow chases the mouse. The cow is green. The cow sees the lion. The dog is kind. The dog sees the mouse. The lion is green. The lion is kind. The mouse chases the lion. The mouse needs the cow. The mouse sees the dog. The mouse sees the lion. If someone needs the cow then they need the dog. If someone needs the lion and they need the mouse then they are young. If someone is red then they need the mouse. If someone sees the dog and the dog chases the cow then they are green. If someone sees the mouse and the mouse needs the dog then the dog is red. If someone needs the mouse and the mouse sees the dog then they need the cow. If someone chases the dog and the dog is green then they are young. If someone sees the lion and the lion chases the dog then they are green. If the mouse chases the cow and the mouse is young then the mouse chases the lion.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow is green.
("cow" "is" "green" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If someone needs the cow then they need the dog.
((("someone" "needs" "cow" "+")) -> ("someone" "needs" "dog" "+"))
If someone needs the lion and they need the mouse then they are young.
((("someone" "needs" "lion" "+") ("someone" "needs" "mouse" "+")) -> ("someone" "is" "young" "+"))
If someone is red then they need the mouse.
((("someone" "is" "red" "+")) -> ("someone" "needs" "mouse" "+"))
If someone sees the dog and the dog chases the cow then they are green.
((("someone" "sees" "dog" "+") ("dog" "chases" "cow" "+")) -> ("someone" "is" "green" "+"))
If someone sees the mouse and the mouse needs the dog then the dog is red.
((("someone" "sees" "mouse" "+") ("mouse" "needs" "dog" "+")) -> ("dog" "is" "red" "+"))
If someone needs the mouse and the mouse sees the dog then they need the cow.
((("someone" "needs" "mouse" "+") ("mouse" "sees" "dog" "+")) -> ("someone" "needs" "cow" "+"))
If someone chases the dog and the dog is green then they are young.
((("someone" "chases" "dog" "+") ("dog" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone sees the lion and the lion chases the dog then they are green.
((("someone" "sees" "lion" "+") ("lion" "chases" "dog" "+")) -> ("someone" "is" "green" "+"))
If the mouse chases the cow and the mouse is young then the mouse chases the lion.
((("mouse" "chases" "cow" "+") ("mouse" "is" "young" "+")) -> ("mouse" "chases" "lion" "+"))
The cow chases the mouse.
True
1
proof
[(triple1)]
("cow" "chases" "mouse" "+")
triple1
The lion is not kind.
False
1
inv-proof
[(triple7)]
("lion" "is" "kind" "-")
triple7
The mouse needs the dog.
True
2
proof
[(((triple9) -> rule1))]
("mouse" "needs" "dog" "+")
((triple9) -> (rule1 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse does not need the dog.
False
2
inv-proof
[(((triple9) -> rule1))]
("mouse" "needs" "dog" "-")
((triple9) -> (rule1 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The dog is red.
True
4
proof
[(((triple5 ((triple9) -> rule1)) -> rule5))]
("dog" "is" "red" "+")
((triple5 ((triple9) -> (rule1 % int2))) -> (rule5 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The dog is not red.
False
4
inv-proof
[(((triple5 ((triple9) -> rule1)) -> rule5))]
("dog" "is" "red" "-")
((triple5 ((triple9) -> (rule1 % int2))) -> (rule5 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The dog needs the mouse.
True
5
proof
[(((((triple5 ((triple9) -> rule1)) -> rule5)) -> rule3))]
("dog" "needs" "mouse" "+")
((((triple5 ((triple9) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The dog does not need the mouse.
False
5
inv-proof
[(((((triple5 ((triple9) -> rule1)) -> rule5)) -> rule3))]
("dog" "needs" "mouse" "-")
((((triple5 ((triple9) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The dog needs the cow.
True
7
proof
[(((((((triple5 ((triple9) -> rule1)) -> rule5)) -> rule3) triple10) -> rule6))]
("dog" "needs" "cow" "+")
((((((triple5 ((triple9) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple10) -> (rule6 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int4
The dog does not need the cow.
False
7
inv-proof
[(((((((triple5 ((triple9) -> rule1)) -> rule5)) -> rule3) triple10) -> rule6))]
("dog" "needs" "cow" "-")
((((((triple5 ((triple9) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple10) -> (rule6 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int4
The dog needs the dog.
True
8
proof
[(((((((((triple5 ((triple9) -> rule1)) -> rule5)) -> rule3) triple10) -> rule6)) -> rule1))]
("dog" "needs" "dog" "+")
((((((((triple5 ((triple9) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int3)) triple10) -> (rule6 % int2))) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
The dog is red.
("dog" "is" "red" "+")
int4
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int5
The dog does not need the dog.
False
8
inv-proof
[(((((((((triple5 ((triple9) -> rule1)) -> rule5)) -> rule3) triple10) -> rule6)) -> rule1))]
("dog" "needs" "dog" "-")
((((((((triple5 ((triple9) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int3)) triple10) -> (rule6 % int2))) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
The dog is red.
("dog" "is" "red" "+")
int4
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int5
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse is young.
Unknown
rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "young" "+")
The cow does not need the cow.
Unknown
inv-rconc
[@2: The cow needs the cow.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("cow" "needs" "cow" "-")
The cow is young.
Unknown
rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "young" "+")
The lion is not young.
Unknown
inv-rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "young" "-")
The mouse is green.
Unknown
rconc
[@1: The mouse is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "green" "+")
The dog does not chase the lion.
Unknown
inv-random
[@0: The dog chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "lion" "-")
The cow sees the mouse.
Unknown
random
[@0: The cow sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "mouse" "+")
The mouse does not chase the dog.
Unknown
inv-random
[@0: The mouse chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "dog" "-")
The lion chases the dog.
Unknown
random
[@0: The lion chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "dog" "+")
The lion does not see the dog.
Unknown
inv-random
[@0: The lion sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "dog" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow chases the mouse.[(triple1)] The cow is green.[(triple2)] The cow sees the lion.[(triple3)] The dog is kind.[(triple4)] The dog sees the mouse.[(triple5)] The lion is green.[(triple6)] The lion is kind.[(triple7)] The mouse chases the lion.[(triple8)] The mouse needs the cow.[(triple9)] The mouse sees the dog.[(triple10)] The mouse sees the lion.[(triple11)] @1: The mouse needs the dog.[(((triple9) -> rule1))] @2: The dog is red.[(((triple5 ((triple9) -> rule1)) -> rule5))] @3: The dog needs the mouse.[(((((triple5 ((triple9) -> rule1)) -> rule5)) -> rule3))] @4: The dog needs the cow.[(((((((triple5 ((triple9) -> rule1)) -> rule5)) -> rule3) triple10) -> rule6))] @5: The dog needs the dog.[(((((((((triple5 ((triple9) -> rule1)) -> rule5)) -> rule3) triple10) -> rule6)) -> rule1))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
The cow sees the lion.
("cow" "sees" "lion" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple5
The lion is green.
("lion" "is" "green" "+")
triple6
The lion is kind.
("lion" "is" "kind" "+")
triple7
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple8
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple9
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple10
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple11
The mouse needs the dog.
("mouse" "needs" "dog" "+")
((triple9) -> (rule1 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
((triple5 ((triple9) -> (rule1 % int2))) -> (rule5 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
((((triple5 ((triple9) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The dog needs the cow.
("dog" "needs" "cow" "+")
((((((triple5 ((triple9) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple10) -> (rule6 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int4
The dog needs the dog.
("dog" "needs" "dog" "+")
((((((((triple5 ((triple9) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int3)) triple10) -> (rule6 % int2))) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
The dog is red.
("dog" "is" "red" "+")
int4
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int5