The dog eats the lion. The dog eats the tiger. The dog does not like the lion. The dog needs the tiger. The lion eats the dog. The lion is kind. The lion is nice. The lion is red. The lion likes the tiger. The lion needs the dog. The lion does not need the squirrel. The lion needs the tiger. The squirrel eats the tiger. The squirrel is red. The squirrel needs the lion. The tiger likes the dog. If the lion is not nice then the lion eats the dog. If something needs the dog and it needs the lion then the dog is kind. If something is blue and it needs the tiger then it likes the tiger. All kind things are blue. If something needs the tiger then it needs the lion. If the squirrel eats the tiger and the squirrel is not rough then the tiger is blue. If something likes the tiger and the tiger is nice then it needs the dog. If the lion likes the tiger then the tiger likes the dog.
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog does not like the lion.
("dog" "likes" "lion" "-")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion does not need the squirrel.
("lion" "needs" "squirrel" "-")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
If the lion is not nice then the lion eats the dog.
((("lion" "is" "nice" "~")) -> ("lion" "eats" "dog" "+"))
If something needs the dog and it needs the lion then the dog is kind.
((("something" "needs" "dog" "+") ("something" "needs" "lion" "+")) -> ("dog" "is" "kind" "+"))
If something is blue and it needs the tiger then it likes the tiger.
((("something" "is" "blue" "+") ("something" "needs" "tiger" "+")) -> ("something" "likes" "tiger" "+"))
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If something needs the tiger then it needs the lion.
((("something" "needs" "tiger" "+")) -> ("something" "needs" "lion" "+"))
If the squirrel eats the tiger and the squirrel is not rough then the tiger is blue.
((("squirrel" "eats" "tiger" "+") ("squirrel" "is" "rough" "~")) -> ("tiger" "is" "blue" "+"))
If something likes the tiger and the tiger is nice then it needs the dog.
((("something" "likes" "tiger" "+") ("tiger" "is" "nice" "+")) -> ("something" "needs" "dog" "+"))
If the lion likes the tiger then the tiger likes the dog.
((("lion" "likes" "tiger" "+")) -> ("tiger" "likes" "dog" "+"))
The dog needs the tiger.
True
1
proof
[(triple4)]
("dog" "needs" "tiger" "+")
triple4
The dog likes the lion.
False
1
inv-proof
[(triple3)]
("dog" "likes" "lion" "+")
triple3
The lion is blue.
True
2
proof
[(((triple6) -> rule4))]
("lion" "is" "blue" "+")
((triple6) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is not blue.
False
2
inv-proof
[(((triple6) -> rule4))]
("lion" "is" "blue" "-")
((triple6) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The dog is kind.
True
4
proof
[(((triple10 ((triple12) -> rule5)) -> rule2))]
("dog" "is" "kind" "+")
((triple10 ((triple12) -> (rule5 % int2))) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The dog is not kind.
False
4
inv-proof
[(((triple10 ((triple12) -> rule5)) -> rule2))]
("dog" "is" "kind" "-")
((triple10 ((triple12) -> (rule5 % int2))) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The dog is blue.
True
5
proof
[(((((triple10 ((triple12) -> rule5)) -> rule2)) -> rule4))]
("dog" "is" "blue" "+")
((((triple10 ((triple12) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
The dog is not blue.
False
5
inv-proof
[(((((triple10 ((triple12) -> rule5)) -> rule2)) -> rule4))]
("dog" "is" "blue" "-")
((((triple10 ((triple12) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
The squirrel does not like the tiger.
Unknown
inv-rconc
[@1: The squirrel likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "likes" "tiger" "-")
The squirrel needs the dog.
Unknown
rconc
[@1: The squirrel needs the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "needs" "dog" "+")
The tiger is not blue.
Unknown
inv-rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "blue" "-")
The tiger needs the lion.
Unknown
rconc
[@1: The tiger needs the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "needs" "lion" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel likes the dog.
Unknown
random
[@0: The squirrel likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "dog" "+")
The dog does not like the squirrel.
Unknown
inv-random
[@0: The dog likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "squirrel" "-")
The lion eats the tiger.
Unknown
random
[@0: The lion eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "tiger" "+")
@0: The dog does not like the lion.[(triple3)] The dog eats the lion.[(triple1)] The dog eats the tiger.[(triple2)] The dog needs the tiger.[(triple4)] The lion does not need the squirrel.[(triple11)] The lion eats the dog.[(triple5)] The lion is kind.[(triple6)] The lion is nice.[(triple7)] The lion is red.[(triple8)] The lion likes the tiger.[(triple9 OR ((((triple6) -> rule4) triple12) -> rule3))] The lion needs the dog.[(triple10)] The lion needs the tiger.[(triple12)] The squirrel eats the tiger.[(triple13)] The squirrel is red.[(triple14)] The squirrel needs the lion.[(triple15)] The tiger likes the dog.[(triple16 OR ((triple9) -> rule8) OR ((((((triple6) -> rule4) triple12) -> rule3)) -> rule8))] @1: The dog needs the lion.[(((triple4) -> rule5))] The lion is blue.[(((triple6) -> rule4))] The lion needs the lion.[(((triple12) -> rule5))] @2: The dog is kind.[(((triple10 ((triple12) -> rule5)) -> rule2))] @3: The dog is blue.[(((((triple10 ((triple12) -> rule5)) -> rule2)) -> rule4))] @4: The dog likes the tiger.[(((((((triple10 ((triple12) -> rule5)) -> rule2)) -> rule4) triple4) -> rule3))]
The dog does not like the lion.
("dog" "likes" "lion" "-")
triple3
The dog eats the lion.
("dog" "eats" "lion" "+")
triple1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple4
The lion does not need the squirrel.
("lion" "needs" "squirrel" "-")
triple11
The lion eats the dog.
("lion" "eats" "dog" "+")
triple5
The lion is kind.
("lion" "is" "kind" "+")
triple6
The lion is nice.
("lion" "is" "nice" "+")
triple7
The lion is red.
("lion" "is" "red" "+")
triple8
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple9
((((triple6) -> (rule4 % int2)) triple12) -> (rule3 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion needs the dog.
("lion" "needs" "dog" "+")
triple10
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple12
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple13
The squirrel is red.
("squirrel" "is" "red" "+")
triple14
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple15
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple16
((triple9) -> (rule8 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
((((((triple6) -> (rule4 % int3)) triple12) -> (rule3 % int2))) -> (rule8 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The dog needs the lion.
("dog" "needs" "lion" "+")
((triple4) -> (rule5 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
((triple6) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple12) -> (rule5 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((triple10 ((triple12) -> (rule5 % int2))) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
((((triple10 ((triple12) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
The dog likes the tiger.
("dog" "likes" "tiger" "+")
((((((triple10 ((triple12) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule4 % int2)) triple4) -> (rule3 % int1))
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The lion needs the lion.
("lion" "needs" "lion" "+")
int4