The cow chases the mouse. The cow is big. The cow is round. The dog likes the mouse. The dog needs the cow. The dog needs the mouse. The lion chases the mouse. The lion likes the mouse. The mouse is big. The mouse likes the cow. If something likes the lion and the lion needs the mouse then the lion needs the cow. All young things are rough. If something needs the cow and it needs the dog then the dog chases the cow. If something is young and it needs the mouse then the mouse likes the dog. If something is round and it chases the lion then the lion chases the mouse. If something likes the dog then it likes the mouse. If something likes the lion and the lion likes the cow then it chases the lion. If something likes the mouse then it is young.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is round.
("cow" "is" "round" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
If something likes the lion and the lion needs the mouse then the lion needs the cow.
((("something" "likes" "lion" "+") ("lion" "needs" "mouse" "+")) -> ("lion" "needs" "cow" "+"))
All young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If something needs the cow and it needs the dog then the dog chases the cow.
((("something" "needs" "cow" "+") ("something" "needs" "dog" "+")) -> ("dog" "chases" "cow" "+"))
If something is young and it needs the mouse then the mouse likes the dog.
((("something" "is" "young" "+") ("something" "needs" "mouse" "+")) -> ("mouse" "likes" "dog" "+"))
If something is round and it chases the lion then the lion chases the mouse.
((("something" "is" "round" "+") ("something" "chases" "lion" "+")) -> ("lion" "chases" "mouse" "+"))
If something likes the dog then it likes the mouse.
((("something" "likes" "dog" "+")) -> ("something" "likes" "mouse" "+"))
If something likes the lion and the lion likes the cow then it chases the lion.
((("something" "likes" "lion" "+") ("lion" "likes" "cow" "+")) -> ("something" "chases" "lion" "+"))
If something likes the mouse then it is young.
((("something" "likes" "mouse" "+")) -> ("something" "is" "young" "+"))
The dog likes the mouse.
True
1
proof
[(triple4)]
("dog" "likes" "mouse" "+")
triple4
The lion does not like the mouse.
False
1
inv-proof
[(triple8)]
("lion" "likes" "mouse" "-")
triple8
The dog is young.
True
2
proof
[(((triple4) -> rule8))]
("dog" "is" "young" "+")
((triple4) -> (rule8 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is not young.
False
2
inv-proof
[(((triple4) -> rule8))]
("dog" "is" "young" "-")
((triple4) -> (rule8 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is rough.
True
3
proof
[(((((triple4) -> rule8)) -> rule2))]
("dog" "is" "rough" "+")
((((triple4) -> (rule8 % int2))) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is not rough.
False
3
inv-proof
[(((((triple4) -> rule8)) -> rule2))]
("dog" "is" "rough" "-")
((((triple4) -> (rule8 % int2))) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The mouse likes the mouse.
True
5
proof
[(((((((triple4) -> rule8) triple6) -> rule4)) -> rule6))]
("mouse" "likes" "mouse" "+")
((((((triple4) -> (rule8 % int3)) triple6) -> (rule4 % int2))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The mouse does not like the mouse.
False
5
inv-proof
[(((((((triple4) -> rule8) triple6) -> rule4)) -> rule6))]
("mouse" "likes" "mouse" "-")
((((((triple4) -> (rule8 % int3)) triple6) -> (rule4 % int2))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The mouse is young.
True
6
proof
[(((((((((triple4) -> rule8) triple6) -> rule4)) -> rule6)) -> rule8))]
("mouse" "is" "young" "+")
((((((((triple4) -> (rule8 % int4)) triple6) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
The dog is young.
("dog" "is" "young" "+")
int4
The mouse is not young.
False
6
inv-proof
[(((((((((triple4) -> rule8) triple6) -> rule4)) -> rule6)) -> rule8))]
("mouse" "is" "young" "-")
((((((((triple4) -> (rule8 % int4)) triple6) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
The dog is young.
("dog" "is" "young" "+")
int4
The mouse is rough.
True
7
proof
[(((((((((((triple4) -> rule8) triple6) -> rule4)) -> rule6)) -> rule8)) -> rule2))]
("mouse" "is" "rough" "+")
((((((((((triple4) -> (rule8 % int5)) triple6) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int4
The dog is young.
("dog" "is" "young" "+")
int5
The mouse is not rough.
False
7
inv-proof
[(((((((((((triple4) -> rule8) triple6) -> rule4)) -> rule6)) -> rule8)) -> rule2))]
("mouse" "is" "rough" "-")
((((((((((triple4) -> (rule8 % int5)) triple6) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int4
The dog is young.
("dog" "is" "young" "+")
int5
The dog does not chase the cow.
Unknown
inv-rconc
[@1: The dog chases the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "cow" "-")
The cow is rough.
Unknown
rconc
[@3: The cow is rough.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule6 <- FAIL)]]
("cow" "is" "rough" "+")
The mouse does not chase the lion.
Unknown
inv-rconc
[@1: The mouse chases the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "chases" "lion" "-")
The cow is young.
Unknown
rconc
[@2: The cow is young.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("cow" "is" "young" "+")
The dog does not chase the lion.
Unknown
inv-rconc
[@1: The dog chases the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "chases" "lion" "-")
The lion chases the lion.
Unknown
rconc
[@1: The lion chases the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "chases" "lion" "+")
The cow does not need the lion.
Unknown
inv-random
[@0: The cow needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "lion" "-")
The cow chases the dog.
Unknown
random
[@0: The cow chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "dog" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (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 dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The cow chases the mouse.[(triple1)] The cow is big.[(triple2)] The cow is round.[(triple3)] The dog likes the mouse.[(triple4)] The dog needs the cow.[(triple5)] The dog needs the mouse.[(triple6)] The lion chases the mouse.[(triple7)] The lion likes the mouse.[(triple8)] The mouse is big.[(triple9)] The mouse likes the cow.[(triple10)] @1: The dog is young.[(((triple4) -> rule8))] The lion is young.[(((triple8) -> rule8))] @2: The dog is rough.[(((((triple4) -> rule8)) -> rule2))] The lion is rough.[(((((triple8) -> rule8)) -> rule2))] The mouse likes the dog.[(((((triple4) -> rule8) triple6) -> rule4))] @3: The mouse likes the mouse.[(((((((triple4) -> rule8) triple6) -> rule4)) -> rule6))] @4: The mouse is young.[(((((((((triple4) -> rule8) triple6) -> rule4)) -> rule6)) -> rule8))] @5: The mouse is rough.[(((((((((((triple4) -> rule8) triple6) -> rule4)) -> rule6)) -> rule8)) -> rule2))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is round.
("cow" "is" "round" "+")
triple3
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple4
The dog needs the cow.
("dog" "needs" "cow" "+")
triple5
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple6
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple7
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple8
The mouse is big.
("mouse" "is" "big" "+")
triple9
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple10
The dog is young.
("dog" "is" "young" "+")
((triple4) -> (rule8 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The lion is young.
("lion" "is" "young" "+")
((triple8) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
((((triple4) -> (rule8 % int2))) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
((((triple8) -> (rule8 % int2))) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
((((triple4) -> (rule8 % int2)) triple6) -> (rule4 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((((triple4) -> (rule8 % int3)) triple6) -> (rule4 % int2))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
((((((((triple4) -> (rule8 % int4)) triple6) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
The dog is young.
("dog" "is" "young" "+")
int4
The mouse is rough.
("mouse" "is" "rough" "+")
((((((((((triple4) -> (rule8 % int5)) triple6) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int4
The dog is young.
("dog" "is" "young" "+")
int5