The cat chases the tiger. The cat is not kind. The cat likes the tiger. The dog is kind. The dog likes the lion. The lion chases the dog. The lion is cold. The lion is green. The lion is round. The lion sees the cat. The lion sees the tiger. The tiger chases the dog. The tiger is green. The tiger likes the dog. The tiger sees the dog. If someone is kind and they like the dog then the dog is round. If someone is green then they chase the tiger. If someone chases the dog and they see the tiger then the tiger sees the lion. If someone sees the tiger and they see the dog then the tiger is kind. If someone sees the tiger then the tiger likes the dog. If someone is cold then they see the dog.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is not kind.
("cat" "is" "kind" "-")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is round.
("lion" "is" "round" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If someone is kind and they like the dog then the dog is round.
((("someone" "is" "kind" "+") ("someone" "likes" "dog" "+")) -> ("dog" "is" "round" "+"))
If someone is green then they chase the tiger.
((("someone" "is" "green" "+")) -> ("someone" "chases" "tiger" "+"))
If someone chases the dog and they see the tiger then the tiger sees the lion.
((("someone" "chases" "dog" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "sees" "lion" "+"))
If someone sees the tiger and they see the dog then the tiger is kind.
((("someone" "sees" "tiger" "+") ("someone" "sees" "dog" "+")) -> ("tiger" "is" "kind" "+"))
If someone sees the tiger then the tiger likes the dog.
((("someone" "sees" "tiger" "+")) -> ("tiger" "likes" "dog" "+"))
If someone is cold then they see the dog.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "dog" "+"))
The lion is cold.
True
1
proof
[(triple7)]
("lion" "is" "cold" "+")
triple7
The lion does not chase the dog.
False
1
inv-proof
[(triple6)]
("lion" "chases" "dog" "-")
triple6
The tiger sees the lion.
True
3
proof
[(((triple6 triple11) -> rule3))]
("tiger" "sees" "lion" "+")
((triple6 triple11) -> (rule3 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The lion does not chase the tiger.
False
2
inv-proof
[(((triple8) -> rule2))]
("lion" "chases" "tiger" "-")
((triple8) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The tiger is kind.
True
4
proof
[(((triple11 ((triple7) -> rule6)) -> rule4))]
("tiger" "is" "kind" "+")
((triple11 ((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
int2
The tiger is not kind.
False
4
inv-proof
[(((triple11 ((triple7) -> rule6)) -> rule4))]
("tiger" "is" "kind" "-")
((triple11 ((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
int2
The dog is round.
True
6
proof
[(((((triple11 ((triple7) -> rule6)) -> rule4) triple14) -> rule1) OR ((((triple11 ((triple7) -> rule6)) -> rule4) ((triple11) -> rule5)) -> rule1))]
("dog" "is" "round" "+")
((((triple11 ((triple7) -> (rule6 % int3))) -> (rule4 % int2)) triple14) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
int3
((((triple11 ((triple7) -> (rule6 % int4))) -> (rule4 % int3)) ((triple11) -> (rule5 % int2))) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The lion sees the dog.
("lion" "sees" "dog" "+")
int4
The dog is not round.
False
6
inv-proof
[(((((triple11 ((triple7) -> rule6)) -> rule4) triple14) -> rule1) OR ((((triple11 ((triple7) -> rule6)) -> rule4) ((triple11) -> rule5)) -> rule1))]
("dog" "is" "round" "-")
((((triple11 ((triple7) -> (rule6 % int3))) -> (rule4 % int2)) triple14) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
int3
((((triple11 ((triple7) -> (rule6 % int4))) -> (rule4 % int3)) ((triple11) -> (rule5 % int2))) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The lion sees the dog.
("lion" "sees" "dog" "+")
int4
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "sees" "dog" "-")
The dog chases the tiger.
Unknown
rconc
[@1: The dog chases the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "tiger" "+")
The cat does not see the dog.
Unknown
inv-rconc
[@1: The cat sees the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "sees" "dog" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "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 chases the cat.
Unknown
random
[@0: The dog chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "cat" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The tiger chases the cat.
Unknown
random
[@0: The tiger chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cat" "+")
@0: The cat chases the tiger.[(triple1)] The cat is not kind.[(triple2)] The cat likes the tiger.[(triple3)] The dog is kind.[(triple4)] The dog likes the lion.[(triple5)] The lion chases the dog.[(triple6)] The lion is cold.[(triple7)] The lion is green.[(triple8)] The lion is round.[(triple9)] The lion sees the cat.[(triple10)] The lion sees the tiger.[(triple11)] The tiger chases the dog.[(triple12)] The tiger is green.[(triple13)] The tiger likes the dog.[(triple14 OR ((triple11) -> rule5))] The tiger sees the dog.[(triple15)] @1: The lion chases the tiger.[(((triple8) -> rule2))] The lion sees the dog.[(((triple7) -> rule6))] The tiger chases the tiger.[(((triple13) -> rule2))] The tiger sees the lion.[(((triple6 triple11) -> rule3))] @2: The tiger is kind.[(((triple11 ((triple7) -> rule6)) -> rule4))] @3: The dog is round.[(((((triple11 ((triple7) -> rule6)) -> rule4) triple14) -> rule1) OR ((((triple11 ((triple7) -> rule6)) -> rule4) ((triple11) -> rule5)) -> rule1))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat is not kind.
("cat" "is" "kind" "-")
triple2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The dog likes the lion.
("dog" "likes" "lion" "+")
triple5
The lion chases the dog.
("lion" "chases" "dog" "+")
triple6
The lion is cold.
("lion" "is" "cold" "+")
triple7
The lion is green.
("lion" "is" "green" "+")
triple8
The lion is round.
("lion" "is" "round" "+")
triple9
The lion sees the cat.
("lion" "sees" "cat" "+")
triple10
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple11
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple12
The tiger is green.
("tiger" "is" "green" "+")
triple13
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple14
((triple11) -> (rule5 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple15
The lion chases the tiger.
("lion" "chases" "tiger" "+")
((triple8) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
((triple7) -> (rule6 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple13) -> (rule2 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
((triple6 triple11) -> (rule3 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple11 ((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
int2
The dog is round.
("dog" "is" "round" "+")
((((triple11 ((triple7) -> (rule6 % int3))) -> (rule4 % int2)) triple14) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
int3
((((triple11 ((triple7) -> (rule6 % int4))) -> (rule4 % int3)) ((triple11) -> (rule5 % int2))) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The lion sees the dog.
("lion" "sees" "dog" "+")
int4