The cat eats the lion. The cat likes the dog. The cat needs the cow. The cow eats the cat. The cow is cold. The cow is nice. The cow likes the dog. The cow likes the lion. The dog is cold. The dog needs the cat. The dog needs the cow. The dog needs the lion. The lion eats the cat. The lion eats the dog. The lion is green. The lion likes the dog. All young things are cold. If something eats the lion and it likes the lion then it is blue. If something needs the cat and the cat eats the cow then it likes the dog. If something likes the dog and it likes the cat then the dog likes the lion. If something eats the dog then it eats the cow. If something eats the cow then it is young. If something likes the cow then the cow is cold. If something needs the cow and it likes the cow then the cow needs the dog. If something likes the dog then it eats the dog.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is green.
("lion" "is" "green" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something eats the lion and it likes the lion then it is blue.
((("something" "eats" "lion" "+") ("something" "likes" "lion" "+")) -> ("something" "is" "blue" "+"))
If something needs the cat and the cat eats the cow then it likes the dog.
((("something" "needs" "cat" "+") ("cat" "eats" "cow" "+")) -> ("something" "likes" "dog" "+"))
If something likes the dog and it likes the cat then the dog likes the lion.
((("something" "likes" "dog" "+") ("something" "likes" "cat" "+")) -> ("dog" "likes" "lion" "+"))
If something eats the dog then it eats the cow.
((("something" "eats" "dog" "+")) -> ("something" "eats" "cow" "+"))
If something eats the cow then it is young.
((("something" "eats" "cow" "+")) -> ("something" "is" "young" "+"))
If something likes the cow then the cow is cold.
((("something" "likes" "cow" "+")) -> ("cow" "is" "cold" "+"))
If something needs the cow and it likes the cow then the cow needs the dog.
((("something" "needs" "cow" "+") ("something" "likes" "cow" "+")) -> ("cow" "needs" "dog" "+"))
If something likes the dog then it eats the dog.
((("something" "likes" "dog" "+")) -> ("something" "eats" "dog" "+"))
The dog needs the lion.
True
1
proof
[(triple12)]
("dog" "needs" "lion" "+")
triple12
The cat does not eat the lion.
False
1
inv-proof
[(triple1)]
("cat" "eats" "lion" "-")
triple1
The cat eats the dog.
True
2
proof
[(((triple2) -> rule9))]
("cat" "eats" "dog" "+")
((triple2) -> (rule9 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The lion does not eat the cow.
False
2
inv-proof
[(((triple14) -> rule5) OR ((((triple16) -> rule9)) -> rule5))]
("lion" "eats" "cow" "-")
((triple14) -> (rule5 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
((((triple16) -> (rule9 % int2))) -> (rule5 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The lion eats the dog.
("lion" "eats" "dog" "+")
int2
The lion is young.
True
3
proof
[(((((triple14) -> rule5)) -> rule6) OR ((((((triple16) -> rule9)) -> rule5)) -> rule6))]
("lion" "is" "young" "+")
((((triple14) -> (rule5 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
((((((triple16) -> (rule9 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The lion eats the dog.
("lion" "eats" "dog" "+")
int3
The cat does not eat the cow.
False
3
inv-proof
[(((((triple2) -> rule9)) -> rule5))]
("cat" "eats" "cow" "-")
((((triple2) -> (rule9 % int2))) -> (rule5 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat eats the dog.
("cat" "eats" "dog" "+")
int2
The dog likes the dog.
True
5
proof
[(((triple10 ((((triple2) -> rule9)) -> rule5)) -> rule3))]
("dog" "likes" "dog" "+")
((triple10 ((((triple2) -> (rule9 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat eats the dog.
("cat" "eats" "dog" "+")
int3
The cat is not young.
False
4
inv-proof
[(((((((triple2) -> rule9)) -> rule5)) -> rule6))]
("cat" "is" "young" "-")
((((((triple2) -> (rule9 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat eats the dog.
("cat" "eats" "dog" "+")
int3
The cat is cold.
True
5
proof
[(((((((((triple2) -> rule9)) -> rule5)) -> rule6)) -> rule1))]
("cat" "is" "cold" "+")
((((((((triple2) -> (rule9 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
int3
The cat eats the dog.
("cat" "eats" "dog" "+")
int4
The cat is not cold.
False
5
inv-proof
[(((((((((triple2) -> rule9)) -> rule5)) -> rule6)) -> rule1))]
("cat" "is" "cold" "-")
((((((((triple2) -> (rule9 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
int3
The cat eats the dog.
("cat" "eats" "dog" "+")
int4
The dog eats the cow.
True
7
proof
[(((((((triple10 ((((triple2) -> rule9)) -> rule5)) -> rule3)) -> rule9)) -> rule5))]
("dog" "eats" "cow" "+")
((((((triple10 ((((triple2) -> (rule9 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule5 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3
The cat eats the cow.
("cat" "eats" "cow" "+")
int4
The cat eats the dog.
("cat" "eats" "dog" "+")
int5
The dog does not eat the cow.
False
7
inv-proof
[(((((((triple10 ((((triple2) -> rule9)) -> rule5)) -> rule3)) -> rule9)) -> rule5))]
("dog" "eats" "cow" "-")
((((((triple10 ((((triple2) -> (rule9 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule5 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3
The cat eats the cow.
("cat" "eats" "cow" "+")
int4
The cat eats the dog.
("cat" "eats" "dog" "+")
int5
The lion is not blue.
Unknown
inv-rconc
[@1: The lion is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "blue" "-")
The cow needs the dog.
Unknown
rconc
[@1: The cow needs the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "needs" "dog" "+")
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "blue" "-")
The dog is blue.
Unknown
rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "blue" "+")
The dog does not like the lion.
Unknown
inv-rconc
[@1: The dog likes the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "likes" "lion" "-")
The cow is blue.
Unknown
rconc
[@1: The cow is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "blue" "+")
The lion does not need the cat.
Unknown
inv-random
[@0: The lion needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cat" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The dog likes the cat.
Unknown
random
[@0: The dog likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cat" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The cat eats the lion.[(triple1)] The cat likes the dog.[(triple2)] The cat needs the cow.[(triple3)] The cow eats the cat.[(triple4)] The cow is cold.[(triple5 OR ((((((((triple7) -> rule9)) -> rule5)) -> rule6)) -> rule1))] The cow is nice.[(triple6)] The cow likes the dog.[(triple7)] The cow likes the lion.[(triple8)] The dog is cold.[(triple9 OR ((((((((((triple10 ((((triple2) -> rule9)) -> rule5)) -> rule3)) -> rule9)) -> rule5)) -> rule6)) -> rule1))] The dog needs the cat.[(triple10)] The dog needs the cow.[(triple11)] The dog needs the lion.[(triple12)] The lion eats the cat.[(triple13)] The lion eats the dog.[(triple14 OR ((triple16) -> rule9))] The lion is green.[(triple15)] The lion likes the dog.[(triple16)] @1: The cat eats the dog.[(((triple2) -> rule9))] The cow eats the dog.[(((triple7) -> rule9))] The lion eats the cow.[(((triple14) -> rule5) OR ((((triple16) -> rule9)) -> rule5))] @2: The cat eats the cow.[(((((triple2) -> rule9)) -> rule5))] The cow eats the cow.[(((((triple7) -> rule9)) -> rule5))] The lion is young.[(((((triple14) -> rule5)) -> rule6) OR ((((((triple16) -> rule9)) -> rule5)) -> rule6))] @3: The cat is young.[(((((((triple2) -> rule9)) -> rule5)) -> rule6))] The cow is young.[(((((((triple7) -> rule9)) -> rule5)) -> rule6))] The dog likes the dog.[(((triple10 ((((triple2) -> rule9)) -> rule5)) -> rule3))] The lion is cold.[(((((((triple14) -> rule5)) -> rule6)) -> rule1) OR ((((((((triple16) -> rule9)) -> rule5)) -> rule6)) -> rule1))] @4: The cat is cold.[(((((((((triple2) -> rule9)) -> rule5)) -> rule6)) -> rule1))] The dog eats the dog.[(((((triple10 ((((triple2) -> rule9)) -> rule5)) -> rule3)) -> rule9))] @5: The dog eats the cow.[(((((((triple10 ((((triple2) -> rule9)) -> rule5)) -> rule3)) -> rule9)) -> rule5))] @6: The dog is young.[(((((((((triple10 ((((triple2) -> rule9)) -> rule5)) -> rule3)) -> rule9)) -> rule5)) -> rule6))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat likes the dog.
("cat" "likes" "dog" "+")
triple2
The cat needs the cow.
("cat" "needs" "cow" "+")
triple3
The cow eats the cat.
("cow" "eats" "cat" "+")
triple4
The cow is cold.
("cow" "is" "cold" "+")
triple5
((((((((triple7) -> (rule9 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The cow eats the dog.
("cow" "eats" "dog" "+")
int4
The cow is nice.
("cow" "is" "nice" "+")
triple6
The cow likes the dog.
("cow" "likes" "dog" "+")
triple7
The cow likes the lion.
("cow" "likes" "lion" "+")
triple8
The dog is cold.
("dog" "is" "cold" "+")
triple9
((((((((((triple10 ((((triple2) -> (rule9 % int7))) -> (rule5 % int6))) -> (rule3 % int5))) -> (rule9 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog eats the cow.
("dog" "eats" "cow" "+")
int3
The dog eats the dog.
("dog" "eats" "dog" "+")
int4
The dog likes the dog.
("dog" "likes" "dog" "+")
int5
The cat eats the cow.
("cat" "eats" "cow" "+")
int6
The cat eats the dog.
("cat" "eats" "dog" "+")
int7
The dog needs the cat.
("dog" "needs" "cat" "+")
triple10
The dog needs the cow.
("dog" "needs" "cow" "+")
triple11
The dog needs the lion.
("dog" "needs" "lion" "+")
triple12
The lion eats the cat.
("lion" "eats" "cat" "+")
triple13
The lion eats the dog.
("lion" "eats" "dog" "+")
triple14
((triple16) -> (rule9 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
The lion is green.
("lion" "is" "green" "+")
triple15
The lion likes the dog.
("lion" "likes" "dog" "+")
triple16
The cat eats the dog.
("cat" "eats" "dog" "+")
((triple2) -> (rule9 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
((triple7) -> (rule9 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
((triple14) -> (rule5 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
((((triple16) -> (rule9 % int2))) -> (rule5 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The lion eats the dog.
("lion" "eats" "dog" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
((((triple2) -> (rule9 % int2))) -> (rule5 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat eats the dog.
("cat" "eats" "dog" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
((((triple7) -> (rule9 % int2))) -> (rule5 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The lion is young.
("lion" "is" "young" "+")
((((triple14) -> (rule5 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
((((((triple16) -> (rule9 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The lion eats the dog.
("lion" "eats" "dog" "+")
int3
The cat is young.
("cat" "is" "young" "+")
((((((triple2) -> (rule9 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat eats the dog.
("cat" "eats" "dog" "+")
int3
The cow is young.
("cow" "is" "young" "+")
((((((triple7) -> (rule9 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow eats the dog.
("cow" "eats" "dog" "+")
int3
The dog likes the dog.
("dog" "likes" "dog" "+")
((triple10 ((((triple2) -> (rule9 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat eats the dog.
("cat" "eats" "dog" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
((((((triple14) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion eats the cow.
("lion" "eats" "cow" "+")
int3
((((((((triple16) -> (rule9 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion eats the cow.
("lion" "eats" "cow" "+")
int3
The lion eats the dog.
("lion" "eats" "dog" "+")
int4
The cat is cold.
("cat" "is" "cold" "+")
((((((((triple2) -> (rule9 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
int3
The cat eats the dog.
("cat" "eats" "dog" "+")
int4
The dog eats the dog.
("dog" "eats" "dog" "+")
((((triple10 ((((triple2) -> (rule9 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
int3
The cat eats the dog.
("cat" "eats" "dog" "+")
int4
The dog eats the cow.
("dog" "eats" "cow" "+")
((((((triple10 ((((triple2) -> (rule9 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule5 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3
The cat eats the cow.
("cat" "eats" "cow" "+")
int4
The cat eats the dog.
("cat" "eats" "dog" "+")
int5
The dog is young.
("dog" "is" "young" "+")
((((((((triple10 ((((triple2) -> (rule9 % int6))) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
int3
The dog likes the dog.
("dog" "likes" "dog" "+")
int4
The cat eats the cow.
("cat" "eats" "cow" "+")
int5
The cat eats the dog.
("cat" "eats" "dog" "+")
int6