The bear is green. The cow is kind. The lion is round. The tiger chases the bear. If something chases the tiger then the tiger is blue. If the cow sees the tiger and the cow chases the tiger then the cow chases the bear. If something is young and round then it eats the lion. Green things are round. If something is kind then it eats the bear. If the bear eats the lion and the lion is kind then the lion sees the cow. If something is round then it chases the bear. If something chases the tiger and the tiger eats the bear then the bear eats the lion.
The bear is green.
("bear" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The lion is round.
("lion" "is" "round" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
If something chases the tiger then the tiger is blue.
((("something" "chases" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
If the cow sees the tiger and the cow chases the tiger then the cow chases the bear.
((("cow" "sees" "tiger" "+") ("cow" "chases" "tiger" "+")) -> ("cow" "chases" "bear" "+"))
If something is young and round then it eats the lion.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "eats" "lion" "+"))
Green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something is kind then it eats the bear.
((("something" "is" "kind" "+")) -> ("something" "eats" "bear" "+"))
If the bear eats the lion and the lion is kind then the lion sees the cow.
((("bear" "eats" "lion" "+") ("lion" "is" "kind" "+")) -> ("lion" "sees" "cow" "+"))
If something is round then it chases the bear.
((("something" "is" "round" "+")) -> ("something" "chases" "bear" "+"))
If something chases the tiger and the tiger eats the bear then the bear eats the lion.
((("something" "chases" "tiger" "+") ("tiger" "eats" "bear" "+")) -> ("bear" "eats" "lion" "+"))
The tiger chases the bear.
True
1
proof
[(triple4)]
("tiger" "chases" "bear" "+")
triple4
The tiger does not chase the bear.
False
1
inv-proof
[(triple4)]
("tiger" "chases" "bear" "-")
triple4
The cow eats the bear.
True
2
proof
[(((triple2) -> rule5))]
("cow" "eats" "bear" "+")
((triple2) -> (rule5 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The bear is not round.
False
2
inv-proof
[(((triple1) -> rule4))]
("bear" "is" "round" "-")
((triple1) -> (rule4 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear chases the bear.
True
3
proof
[(((((triple1) -> rule4)) -> rule7))]
("bear" "chases" "bear" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear does not chase the bear.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule7))]
("bear" "chases" "bear" "-")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The cow does not eat the lion.
Unknown
inv-rconc
[@1: The cow eats the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "eats" "lion" "-")
The cow chases the bear.
Unknown
rconc
[@2: The cow chases the bear.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("cow" "chases" "bear" "+")
The lion does not eat the bear.
Unknown
inv-rconc
[@1: The lion eats the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "eats" "bear" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
@0: The bear is green.[(triple1)] The cow is kind.[(triple2)] The lion is round.[(triple3)] The tiger chases the bear.[(triple4)] @1: The bear is round.[(((triple1) -> rule4))] The cow eats the bear.[(((triple2) -> rule5))] The lion chases the bear.[(((triple3) -> rule7))] @2: The bear chases the bear.[(((((triple1) -> rule4)) -> rule7))]
The bear is green.
("bear" "is" "green" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple4
The bear is round.
("bear" "is" "round" "+")
((triple1) -> (rule4 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
((triple2) -> (rule5 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
((triple3) -> (rule7 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2