The bear chases the dog. The bear chases the tiger. The bear is green. The bear is nice. The dog chases the tiger. The dog eats the tiger. The dog is green. The lion eats the tiger. The lion is round. The tiger chases the bear. If something is green and it eats the lion then the lion is green. If something visits the lion and the lion visits the tiger then the tiger chases the dog. If the bear chases the lion and the lion is nice then the bear is kind. If something is nice then it eats the tiger. If something chases the bear and it visits the bear then it is round. All kind things are rough. If something eats the tiger and the tiger chases the dog then it is green. If something eats the tiger and it chases the dog then the tiger chases the dog.
The bear chases the dog.
("bear" "chases" "dog" "+")
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is nice.
("bear" "is" "nice" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is green.
("dog" "is" "green" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is round.
("lion" "is" "round" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
If something is green and it eats the lion then the lion is green.
((("something" "is" "green" "+") ("something" "eats" "lion" "+")) -> ("lion" "is" "green" "+"))
If something visits the lion and the lion visits the tiger then the tiger chases the dog.
((("something" "visits" "lion" "+") ("lion" "visits" "tiger" "+")) -> ("tiger" "chases" "dog" "+"))
If the bear chases the lion and the lion is nice then the bear is kind.
((("bear" "chases" "lion" "+") ("lion" "is" "nice" "+")) -> ("bear" "is" "kind" "+"))
If something is nice then it eats the tiger.
((("something" "is" "nice" "+")) -> ("something" "eats" "tiger" "+"))
If something chases the bear and it visits the bear then it is round.
((("something" "chases" "bear" "+") ("something" "visits" "bear" "+")) -> ("something" "is" "round" "+"))
All kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something eats the tiger and the tiger chases the dog then it is green.
((("something" "eats" "tiger" "+") ("tiger" "chases" "dog" "+")) -> ("something" "is" "green" "+"))
If something eats the tiger and it chases the dog then the tiger chases the dog.
((("something" "eats" "tiger" "+") ("something" "chases" "dog" "+")) -> ("tiger" "chases" "dog" "+"))
The lion eats the tiger.
True
1
proof
[(triple8)]
("lion" "eats" "tiger" "+")
triple8
The bear is not nice.
False
1
inv-proof
[(triple4)]
("bear" "is" "nice" "-")
triple4
The bear eats the tiger.
True
2
proof
[(((triple4) -> rule4))]
("bear" "eats" "tiger" "+")
((triple4) -> (rule4 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear does not eat the tiger.
False
2
inv-proof
[(((triple4) -> rule4))]
("bear" "eats" "tiger" "-")
((triple4) -> (rule4 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The tiger chases the dog.
True
4
proof
[(((((triple4) -> rule4) triple1) -> rule8))]
("tiger" "chases" "dog" "+")
((((triple4) -> (rule4 % int2)) triple1) -> (rule8 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
The tiger does not chase the dog.
False
4
inv-proof
[(((((triple4) -> rule4) triple1) -> rule8))]
("tiger" "chases" "dog" "-")
((((triple4) -> (rule4 % int2)) triple1) -> (rule8 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
The lion is green.
True
6
proof
[(((triple8 ((((triple4) -> rule4) triple1) -> rule8)) -> rule7))]
("lion" "is" "green" "+")
((triple8 ((((triple4) -> (rule4 % int3)) triple1) -> (rule8 % int2))) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int3
The lion is not green.
False
6
inv-proof
[(((triple8 ((((triple4) -> rule4) triple1) -> rule8)) -> rule7))]
("lion" "is" "green" "-")
((triple8 ((((triple4) -> (rule4 % int3)) triple1) -> (rule8 % int2))) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int3
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "round" "-")
The bear is round.
Unknown
rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "round" "+")
The tiger is not round.
Unknown
inv-rconc
[@1: The tiger is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "round" "-")
The dog is rough.
Unknown
rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "rough" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The lion chases the tiger.
Unknown
random
[@0: The lion chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "tiger" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The dog chases the bear.
Unknown
random
[@0: The dog chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "bear" "+")
@0: The bear chases the dog.[(triple1)] The bear chases the tiger.[(triple2)] The bear is green.[(triple3 OR ((((triple4) -> rule4) ((((triple4) -> rule4) triple1) -> rule8)) -> rule7))] The bear is nice.[(triple4)] The dog chases the tiger.[(triple5)] The dog eats the tiger.[(triple6)] The dog is green.[(triple7 OR ((triple6 ((((triple4) -> rule4) triple1) -> rule8)) -> rule7))] The lion eats the tiger.[(triple8)] The lion is round.[(triple9)] The tiger chases the bear.[(triple10)] @1: The bear eats the tiger.[(((triple4) -> rule4))] @2: The tiger chases the dog.[(((((triple4) -> rule4) triple1) -> rule8))] @3: The lion is green.[(((triple8 ((((triple4) -> rule4) triple1) -> rule8)) -> rule7))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple2
The bear is green.
("bear" "is" "green" "+")
triple3
((((triple4) -> (rule4 % int3)) ((((triple4) -> (rule4 % int3)) triple1) -> (rule8 % int2))) -> (rule7 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
triple4
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple5
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple6
The dog is green.
("dog" "is" "green" "+")
triple7
((triple6 ((((triple4) -> (rule4 % int3)) triple1) -> (rule8 % int2))) -> (rule7 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int3
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple8
The lion is round.
("lion" "is" "round" "+")
triple9
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple10
The bear eats the tiger.
("bear" "eats" "tiger" "+")
((triple4) -> (rule4 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
((((triple4) -> (rule4 % int2)) triple1) -> (rule8 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
The lion is green.
("lion" "is" "green" "+")
((triple8 ((((triple4) -> (rule4 % int3)) triple1) -> (rule8 % int2))) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int3