The bear is big. The cow is round. The lion needs the tiger. The tiger chases the lion. If something chases the lion and it is green then it sees the lion. If something needs the lion then it is not round. If something needs the tiger then it sees the cow. If something needs the cow then it is blue. If something sees the cow then it needs the cow. If the cow does not see the lion and the cow does not chase the tiger then the lion needs the bear.
The bear is big.
("bear" "is" "big" "+")
The cow is round.
("cow" "is" "round" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
If something chases the lion and it is green then it sees the lion.
((("something" "chases" "lion" "+") ("something" "is" "green" "+")) -> ("something" "sees" "lion" "+"))
If something needs the lion then it is not round.
((("something" "needs" "lion" "+")) -> ("something" "is" "round" "-"))
If something needs the tiger then it sees the cow.
((("something" "needs" "tiger" "+")) -> ("something" "sees" "cow" "+"))
If something needs the cow then it is blue.
((("something" "needs" "cow" "+")) -> ("something" "is" "blue" "+"))
If something sees the cow then it needs the cow.
((("something" "sees" "cow" "+")) -> ("something" "needs" "cow" "+"))
If the cow does not see the lion and the cow does not chase the tiger then the lion needs the bear.
((("cow" "sees" "lion" "~") ("cow" "chases" "tiger" "~")) -> ("lion" "needs" "bear" "+"))
The cow is round.
True
1
proof
[(triple2)]
("cow" "is" "round" "+")
triple2
The tiger does not chase the lion.
False
1
inv-proof
[(triple4)]
("tiger" "chases" "lion" "-")
triple4
The lion sees the cow.
True
2
proof
[(((triple3) -> rule3))]
("lion" "sees" "cow" "+")
((triple3) -> (rule3 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion does not see the cow.
False
2
inv-proof
[(((triple3) -> rule3))]
("lion" "sees" "cow" "-")
((triple3) -> (rule3 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion needs the cow.
True
3
proof
[(((((triple3) -> rule3)) -> rule5))]
("lion" "needs" "cow" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion does not need the cow.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule5))]
("lion" "needs" "cow" "-")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion is blue.
True
4
proof
[(((((((triple3) -> rule3)) -> rule5)) -> rule4))]
("lion" "is" "blue" "+")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3
The lion is not blue.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule5)) -> rule4))]
("lion" "is" "blue" "-")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3
The lion does not see the lion.
Unknown
inv-rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "lion" "-")
The bear sees the lion.
Unknown
rconc
[@1: The bear sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "lion" "+")
The tiger does not need the cow.
Unknown
inv-rconc
[@2: The tiger needs the cow.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("tiger" "needs" "cow" "-")
The cow sees the lion.
Unknown
rconc
[@1: The cow sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "lion" "+")
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The cow sees the bear.
Unknown
random
[@0: The cow sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "bear" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The cow needs the lion.
Unknown
random
[@0: The cow needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "lion" "+")
@0: The bear is big.[(triple1)] The cow is round.[(triple2)] The lion needs the tiger.[(triple3)] The tiger chases the lion.[(triple4)] @1: The lion sees the cow.[(((triple3) -> rule3))] @2: The lion needs the cow.[(((((triple3) -> rule3)) -> rule5))] @3: The lion is blue.[(((((((triple3) -> rule3)) -> rule5)) -> rule4))]
The bear is big.
("bear" "is" "big" "+")
triple1
The cow is round.
("cow" "is" "round" "+")
triple2
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple3
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple4
The lion sees the cow.
("lion" "sees" "cow" "+")
((triple3) -> (rule3 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3