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