The bear eats the dog. The bear sees the lion. The cat is green. The cat likes the lion. The dog is big. The dog does not see the cat. The lion eats the bear. The lion eats the dog. The lion is green. The lion likes the cat. The lion sees the bear. The lion sees the dog. If something sees the dog and it is green then the dog eats the cat. If something is green and it does not eat the dog then it is not kind. If something eats the lion and it sees the lion then the lion does not like the dog. If something is big and not green then it is young. If something sees the bear then the bear does not eat the lion. If something eats the bear and the bear is blue then the bear likes the dog. If something eats the bear and the bear does not eat the lion then the bear is blue. If something likes the dog then the dog is young. All young things are blue.
The bear eats the dog.
("bear" "eats" "dog" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The cat is green.
("cat" "is" "green" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The dog is big.
("dog" "is" "big" "+")
The dog does not see the cat.
("dog" "sees" "cat" "-")
The lion eats the bear.
("lion" "eats" "bear" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is green.
("lion" "is" "green" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
If something sees the dog and it is green then the dog eats the cat.
((("something" "sees" "dog" "+") ("something" "is" "green" "+")) -> ("dog" "eats" "cat" "+"))
If something is green and it does not eat the dog then it is not kind.
((("something" "is" "green" "+") ("something" "eats" "dog" "~")) -> ("something" "is" "kind" "-"))
If something eats the lion and it sees the lion then the lion does not like the dog.
((("something" "eats" "lion" "+") ("something" "sees" "lion" "+")) -> ("lion" "likes" "dog" "-"))
If something is big and not green then it is young.
((("something" "is" "big" "+") ("something" "is" "green" "~")) -> ("something" "is" "young" "+"))
If something sees the bear then the bear does not eat the lion.
((("something" "sees" "bear" "+")) -> ("bear" "eats" "lion" "-"))
If something eats the bear and the bear is blue then the bear likes the dog.
((("something" "eats" "bear" "+") ("bear" "is" "blue" "+")) -> ("bear" "likes" "dog" "+"))
If something eats the bear and the bear does not eat the lion then the bear is blue.
((("something" "eats" "bear" "+") ("bear" "eats" "lion" "~")) -> ("bear" "is" "blue" "+"))
If something likes the dog then the dog is young.
((("something" "likes" "dog" "+")) -> ("dog" "is" "young" "+"))
All young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
The lion is green.
True
1
proof
[(triple9)]
("lion" "is" "green" "+")
triple9
The lion does not eat the bear.
False
1
inv-proof
[(triple7)]
("lion" "eats" "bear" "-")
triple7
The bear does not eat the lion.
True
2
proof
[(((triple11) -> rule5))]
("bear" "eats" "lion" "-")
((triple11) -> (rule5 % int1))
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int1
The bear eats the lion.
False
2
inv-proof
[(((triple11) -> rule5))]
("bear" "eats" "lion" "+")
((triple11) -> (rule5 % int1))
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int1
The bear is blue.
True
4
proof
[(((triple7 ((triple11) -> rule5)) -> rule7))]
("bear" "is" "blue" "+")
((triple7 ((triple11) -> (rule5 % int2))) -> (rule7 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int2
The bear is not blue.
False
4
inv-proof
[(((triple7 ((triple11) -> rule5)) -> rule7))]
("bear" "is" "blue" "-")
((triple7 ((triple11) -> (rule5 % int2))) -> (rule7 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int2
The bear likes the dog.
True
6
proof
[(((triple7 ((triple7 ((triple11) -> rule5)) -> rule7)) -> rule6))]
("bear" "likes" "dog" "+")
((triple7 ((triple7 ((triple11) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int3
The bear does not like the dog.
False
6
inv-proof
[(((triple7 ((triple7 ((triple11) -> rule5)) -> rule7)) -> rule6))]
("bear" "likes" "dog" "-")
((triple7 ((triple7 ((triple11) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int3
The dog is young.
True
7
proof
[(((((triple7 ((triple7 ((triple11) -> rule5)) -> rule7)) -> rule6)) -> rule8))]
("dog" "is" "young" "+")
((((triple7 ((triple7 ((triple11) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int4
The dog is not young.
False
7
inv-proof
[(((((triple7 ((triple7 ((triple11) -> rule5)) -> rule7)) -> rule6)) -> rule8))]
("dog" "is" "young" "-")
((((triple7 ((triple7 ((triple11) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int4
The dog is blue.
True
8
proof
[(((((((triple7 ((triple7 ((triple11) -> rule5)) -> rule7)) -> rule6)) -> rule8)) -> rule9))]
("dog" "is" "blue" "+")
((((((triple7 ((triple7 ((triple11) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The bear likes the dog.
("bear" "likes" "dog" "+")
int3
The bear is blue.
("bear" "is" "blue" "+")
int4
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int5
The dog is not blue.
False
8
inv-proof
[(((((((triple7 ((triple7 ((triple11) -> rule5)) -> rule7)) -> rule6)) -> rule8)) -> rule9))]
("dog" "is" "blue" "-")
((((((triple7 ((triple7 ((triple11) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The bear likes the dog.
("bear" "likes" "dog" "+")
int3
The bear is blue.
("bear" "is" "blue" "+")
int4
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int5
The lion is not young.
Unknown
inv-rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "young" "-")
The cat is blue.
Unknown
rconc
[@2: The cat is blue.[CWA. Example of deepest failure = (rule9 <- rule4 <- FAIL)]]
("cat" "is" "blue" "+")
The bear is not young.
Unknown
inv-rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "young" "-")
The lion is blue.
Unknown
rconc
[@2: The lion is blue.[CWA. Example of deepest failure = (rule9 <- rule4 <- FAIL)]]
("lion" "is" "blue" "+")
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "young" "-")
The cat likes the bear.
Unknown
random
[@0: The cat likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "bear" "+")
The cat does not like the dog.
Unknown
inv-random
[@0: The cat likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "dog" "-")
The cat eats the dog.
Unknown
random
[@0: The cat eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "dog" "+")
The cat does not see the bear.
Unknown
inv-random
[@0: The cat sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "bear" "-")
The bear sees the dog.
Unknown
random
[@0: The bear sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "dog" "+")
The dog does not see the bear.
Unknown
inv-random
[@0: The dog sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "bear" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
@0: The bear eats the dog.[(triple1)] The bear sees the lion.[(triple2)] The cat is green.[(triple3)] The cat likes the lion.[(triple4)] The dog does not see the cat.[(triple6)] The dog is big.[(triple5)] The lion eats the bear.[(triple7)] The lion eats the dog.[(triple8)] The lion is green.[(triple9)] The lion likes the cat.[(triple10)] The lion sees the bear.[(triple11)] The lion sees the dog.[(triple12)] @1: The bear does not eat the lion.[(((triple11) -> rule5))] The dog eats the cat.[(((triple12 triple9) -> rule1))] @2: The bear is blue.[(((triple7 ((triple11) -> rule5)) -> rule7))] @3: The bear likes the dog.[(((triple7 ((triple7 ((triple11) -> rule5)) -> rule7)) -> rule6))] @4: The dog is young.[(((((triple7 ((triple7 ((triple11) -> rule5)) -> rule7)) -> rule6)) -> rule8))] @5: The dog is blue.[(((((((triple7 ((triple7 ((triple11) -> rule5)) -> rule7)) -> rule6)) -> rule8)) -> rule9))]
The bear eats the dog.
("bear" "eats" "dog" "+")
triple1
The bear sees the lion.
("bear" "sees" "lion" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat likes the lion.
("cat" "likes" "lion" "+")
triple4
The dog does not see the cat.
("dog" "sees" "cat" "-")
triple6
The dog is big.
("dog" "is" "big" "+")
triple5
The lion eats the bear.
("lion" "eats" "bear" "+")
triple7
The lion eats the dog.
("lion" "eats" "dog" "+")
triple8
The lion is green.
("lion" "is" "green" "+")
triple9
The lion likes the cat.
("lion" "likes" "cat" "+")
triple10
The lion sees the bear.
("lion" "sees" "bear" "+")
triple11
The lion sees the dog.
("lion" "sees" "dog" "+")
triple12
The bear does not eat the lion.
("bear" "eats" "lion" "-")
((triple11) -> (rule5 % int1))
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
((triple12 triple9) -> (rule1 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
((triple7 ((triple11) -> (rule5 % int2))) -> (rule7 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int2
The bear likes the dog.
("bear" "likes" "dog" "+")
((triple7 ((triple7 ((triple11) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int3
The dog is young.
("dog" "is" "young" "+")
((((triple7 ((triple7 ((triple11) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int4
The dog is blue.
("dog" "is" "blue" "+")
((((((triple7 ((triple7 ((triple11) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The bear likes the dog.
("bear" "likes" "dog" "+")
int3
The bear is blue.
("bear" "is" "blue" "+")
int4
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int5