The dog is blue. The dog sees the tiger. The lion chases the tiger. The squirrel chases the lion. The squirrel likes the lion. The tiger likes the lion. The tiger sees the lion. If something sees the tiger then the tiger chases the lion. If something is round then it chases the dog. If something sees the lion and it chases the lion then the lion is round. If something likes the dog then the dog sees the lion. If the squirrel sees the lion and the lion is nice then the squirrel is green. If something sees the lion then the lion sees the squirrel. If something sees the squirrel then the squirrel chases the lion. If the tiger chases the dog then the tiger is green.
The dog is blue.
("dog" "is" "blue" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If something sees the tiger then the tiger chases the lion.
((("something" "sees" "tiger" "+")) -> ("tiger" "chases" "lion" "+"))
If something is round then it chases the dog.
((("something" "is" "round" "+")) -> ("something" "chases" "dog" "+"))
If something sees the lion and it chases the lion then the lion is round.
((("something" "sees" "lion" "+") ("something" "chases" "lion" "+")) -> ("lion" "is" "round" "+"))
If something likes the dog then the dog sees the lion.
((("something" "likes" "dog" "+")) -> ("dog" "sees" "lion" "+"))
If the squirrel sees the lion and the lion is nice then the squirrel is green.
((("squirrel" "sees" "lion" "+") ("lion" "is" "nice" "+")) -> ("squirrel" "is" "green" "+"))
If something sees the lion then the lion sees the squirrel.
((("something" "sees" "lion" "+")) -> ("lion" "sees" "squirrel" "+"))
If something sees the squirrel then the squirrel chases the lion.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "chases" "lion" "+"))
If the tiger chases the dog then the tiger is green.
((("tiger" "chases" "dog" "+")) -> ("tiger" "is" "green" "+"))
The tiger sees the lion.
True
1
proof
[(triple7)]
("tiger" "sees" "lion" "+")
triple7
The squirrel does not chase the lion.
False
1
inv-proof
[(triple4 OR ((((triple7) -> rule6)) -> rule7))]
("squirrel" "chases" "lion" "-")
triple4
((((triple7) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The tiger chases the lion.
True
2
proof
[(((triple2) -> rule1))]
("tiger" "chases" "lion" "+")
((triple2) -> (rule1 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The lion does not see the squirrel.
False
2
inv-proof
[(((triple7) -> rule6))]
("lion" "sees" "squirrel" "-")
((triple7) -> (rule6 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is round.
True
4
proof
[(((triple7 ((triple2) -> rule1)) -> rule3))]
("lion" "is" "round" "+")
((triple7 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The lion is not round.
False
4
inv-proof
[(((triple7 ((triple2) -> rule1)) -> rule3))]
("lion" "is" "round" "-")
((triple7 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The lion chases the dog.
True
5
proof
[(((((triple7 ((triple2) -> rule1)) -> rule3)) -> rule2))]
("lion" "chases" "dog" "+")
((((triple7 ((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int3
The lion does not chase the dog.
False
5
inv-proof
[(((((triple7 ((triple2) -> rule1)) -> rule3)) -> rule2))]
("lion" "chases" "dog" "-")
((((triple7 ((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int3
The tiger is not green.
Unknown
inv-rconc
[@2: The tiger is green.[CWA. Example of deepest failure = (rule8 <- rule2 <- FAIL)]]
("tiger" "is" "green" "-")
The squirrel chases the dog.
Unknown
rconc
[@1: The squirrel chases the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "chases" "dog" "+")
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "dog" "-")
The tiger chases the dog.
Unknown
rconc
[@1: The tiger chases the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "chases" "dog" "+")
The tiger does not see the dog.
Unknown
inv-random
[@0: The tiger sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "dog" "-")
The tiger sees the squirrel.
Unknown
random
[@0: The tiger sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "squirrel" "+")
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The lion likes the tiger.
Unknown
random
[@0: The lion likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "tiger" "+")
@0: The dog is blue.[(triple1)] The dog sees the tiger.[(triple2)] The lion chases the tiger.[(triple3)] The squirrel chases the lion.[(triple4 OR ((((triple7) -> rule6)) -> rule7))] The squirrel likes the lion.[(triple5)] The tiger likes the lion.[(triple6)] The tiger sees the lion.[(triple7)] @1: The lion sees the squirrel.[(((triple7) -> rule6))] The tiger chases the lion.[(((triple2) -> rule1))] @2: The lion is round.[(((triple7 ((triple2) -> rule1)) -> rule3))] @3: The lion chases the dog.[(((((triple7 ((triple2) -> rule1)) -> rule3)) -> rule2))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple3
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple4
((((triple7) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple5
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple6
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple7
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((triple7) -> (rule6 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
((triple2) -> (rule1 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
((triple7 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
((((triple7 ((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int3