The cat is green. The cat needs the dog. The cat needs the lion. The cat visits the dog. The cow eats the dog. The cow is blue. The dog eats the cow. The dog is young. The dog needs the lion. The lion eats the cow. The lion eats the dog. The lion is blue. The lion is young. The lion visits the cow. The lion visits the dog. If the cow visits the cat then the cat eats the dog. If the lion needs the cat and the cat needs the dog then the dog is green. If something eats the cow then it eats the lion. If something visits the lion and the lion is blue then it is young. If something needs the cat and the cat is green then the cat eats the cow. If something visits the cow then it needs the cat. If the cat needs the lion and the lion needs the cat then the cat is round. If the lion eats the dog and the lion needs the cat then the cat visits the dog.
The cat is green.
("cat" "is" "green" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The cow eats the dog.
("cow" "eats" "dog" "+")
The cow is blue.
("cow" "is" "blue" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is young.
("lion" "is" "young" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If the cow visits the cat then the cat eats the dog.
((("cow" "visits" "cat" "+")) -> ("cat" "eats" "dog" "+"))
If the lion needs the cat and the cat needs the dog then the dog is green.
((("lion" "needs" "cat" "+") ("cat" "needs" "dog" "+")) -> ("dog" "is" "green" "+"))
If something eats the cow then it eats the lion.
((("something" "eats" "cow" "+")) -> ("something" "eats" "lion" "+"))
If something visits the lion and the lion is blue then it is young.
((("something" "visits" "lion" "+") ("lion" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something needs the cat and the cat is green then the cat eats the cow.
((("something" "needs" "cat" "+") ("cat" "is" "green" "+")) -> ("cat" "eats" "cow" "+"))
If something visits the cow then it needs the cat.
((("something" "visits" "cow" "+")) -> ("something" "needs" "cat" "+"))
If the cat needs the lion and the lion needs the cat then the cat is round.
((("cat" "needs" "lion" "+") ("lion" "needs" "cat" "+")) -> ("cat" "is" "round" "+"))
If the lion eats the dog and the lion needs the cat then the cat visits the dog.
((("lion" "eats" "dog" "+") ("lion" "needs" "cat" "+")) -> ("cat" "visits" "dog" "+"))
The dog needs the lion.
True
1
proof
[(triple9)]
("dog" "needs" "lion" "+")
triple9
The cat does not need the dog.
False
1
inv-proof
[(triple2)]
("cat" "needs" "dog" "-")
triple2
The lion eats the lion.
True
2
proof
[(((triple10) -> rule3))]
("lion" "eats" "lion" "+")
((triple10) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion does not need the cat.
False
2
inv-proof
[(((triple14) -> rule6))]
("lion" "needs" "cat" "-")
((triple14) -> (rule6 % int1))
The lion needs the cat.
("lion" "needs" "cat" "+")
int1
The dog is green.
True
4
proof
[(((((triple14) -> rule6) triple2) -> rule2))]
("dog" "is" "green" "+")
((((triple14) -> (rule6 % int2)) triple2) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The cat does not eat the cow.
False
4
inv-proof
[(((((triple14) -> rule6) triple1) -> rule5))]
("cat" "eats" "cow" "-")
((((triple14) -> (rule6 % int2)) triple1) -> (rule5 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The cat eats the lion.
True
5
proof
[(((((((triple14) -> rule6) triple1) -> rule5)) -> rule3))]
("cat" "eats" "lion" "+")
((((((triple14) -> (rule6 % int3)) triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The lion needs the cat.
("lion" "needs" "cat" "+")
int3
The cat does not eat the lion.
False
5
inv-proof
[(((((((triple14) -> rule6) triple1) -> rule5)) -> rule3))]
("cat" "eats" "lion" "-")
((((((triple14) -> (rule6 % int3)) triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The lion needs the cat.
("lion" "needs" "cat" "+")
int3
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "needs" "cat" "-")
The cow is young.
Unknown
rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "young" "+")
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "young" "-")
The dog needs the cat.
Unknown
rconc
[@1: The dog needs the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "needs" "cat" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cow needs the lion.
Unknown
random
[@0: The cow needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "lion" "+")
@0: The cat is green.[(triple1)] The cat needs the dog.[(triple2)] The cat needs the lion.[(triple3)] The cat visits the dog.[(triple4 OR ((triple11 ((triple14) -> rule6)) -> rule8))] The cow eats the dog.[(triple5)] The cow is blue.[(triple6)] The dog eats the cow.[(triple7)] The dog is young.[(triple8)] The dog needs the lion.[(triple9)] The lion eats the cow.[(triple10)] The lion eats the dog.[(triple11)] The lion is blue.[(triple12)] The lion is young.[(triple13)] The lion visits the cow.[(triple14)] The lion visits the dog.[(triple15)] @1: The dog eats the lion.[(((triple7) -> rule3))] The lion eats the lion.[(((triple10) -> rule3))] The lion needs the cat.[(((triple14) -> rule6))] @2: The cat eats the cow.[(((((triple14) -> rule6) triple1) -> rule5))] The cat is round.[(((triple3 ((triple14) -> rule6)) -> rule7))] The dog is green.[(((((triple14) -> rule6) triple2) -> rule2))] @3: The cat eats the lion.[(((((((triple14) -> rule6) triple1) -> rule5)) -> rule3))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat needs the dog.
("cat" "needs" "dog" "+")
triple2
The cat needs the lion.
("cat" "needs" "lion" "+")
triple3
The cat visits the dog.
("cat" "visits" "dog" "+")
triple4
((triple11 ((triple14) -> (rule6 % int2))) -> (rule8 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The cow eats the dog.
("cow" "eats" "dog" "+")
triple5
The cow is blue.
("cow" "is" "blue" "+")
triple6
The dog eats the cow.
("dog" "eats" "cow" "+")
triple7
The dog is young.
("dog" "is" "young" "+")
triple8
The dog needs the lion.
("dog" "needs" "lion" "+")
triple9
The lion eats the cow.
("lion" "eats" "cow" "+")
triple10
The lion eats the dog.
("lion" "eats" "dog" "+")
triple11
The lion is blue.
("lion" "is" "blue" "+")
triple12
The lion is young.
("lion" "is" "young" "+")
triple13
The lion visits the cow.
("lion" "visits" "cow" "+")
triple14
The lion visits the dog.
("lion" "visits" "dog" "+")
triple15
The dog eats the lion.
("dog" "eats" "lion" "+")
((triple7) -> (rule3 % int1))
The dog eats the lion.
("dog" "eats" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple10) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
((triple14) -> (rule6 % int1))
The lion needs the cat.
("lion" "needs" "cat" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
((((triple14) -> (rule6 % int2)) triple1) -> (rule5 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
((triple3 ((triple14) -> (rule6 % int2))) -> (rule7 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The dog is green.
("dog" "is" "green" "+")
((((triple14) -> (rule6 % int2)) triple2) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The cat eats the lion.
("cat" "eats" "lion" "+")
((((((triple14) -> (rule6 % int3)) triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The lion needs the cat.
("lion" "needs" "cat" "+")
int3