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