The cow chases the squirrel. The squirrel is blue. The tiger eats the cow. If someone needs the tiger and the tiger is young then they are blue. If someone eats the tiger and they are red then they do not chase the tiger. If someone is kind then they do not chase the tiger. Blue people are green. Green people are kind. If the tiger needs the squirrel then the tiger does not chase the squirrel. If someone is green then they need the cow. If the cow needs the tiger and the cow is kind then the tiger is not green.
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
If someone needs the tiger and the tiger is young then they are blue.
((("someone" "needs" "tiger" "+") ("tiger" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If someone eats the tiger and they are red then they do not chase the tiger.
((("someone" "eats" "tiger" "+") ("someone" "is" "red" "+")) -> ("someone" "chases" "tiger" "-"))
If someone is kind then they do not chase the tiger.
((("someone" "is" "kind" "+")) -> ("someone" "chases" "tiger" "-"))
Blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If the tiger needs the squirrel then the tiger does not chase the squirrel.
((("tiger" "needs" "squirrel" "+")) -> ("tiger" "chases" "squirrel" "-"))
If someone is green then they need the cow.
((("someone" "is" "green" "+")) -> ("someone" "needs" "cow" "+"))
If the cow needs the tiger and the cow is kind then the tiger is not green.
((("cow" "needs" "tiger" "+") ("cow" "is" "kind" "+")) -> ("tiger" "is" "green" "-"))
The cow chases the squirrel.
True
1
proof
[(triple1)]
("cow" "chases" "squirrel" "+")
triple1
The squirrel is not blue.
False
1
inv-proof
[(triple2)]
("squirrel" "is" "blue" "-")
triple2
The squirrel is green.
True
2
proof
[(((triple2) -> rule4))]
("squirrel" "is" "green" "+")
((triple2) -> (rule4 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is not green.
False
2
inv-proof
[(((triple2) -> rule4))]
("squirrel" "is" "green" "-")
((triple2) -> (rule4 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel needs the cow.
True
3
proof
[(((((triple2) -> rule4)) -> rule7))]
("squirrel" "needs" "cow" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel is not kind.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("squirrel" "is" "kind" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel does not chase the tiger.
True
4
proof
[(((((((triple2) -> rule4)) -> rule5)) -> rule3))]
("squirrel" "chases" "tiger" "-")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel does not chase the tiger.
("squirrel" "chases" "tiger" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The squirrel chases the tiger.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule5)) -> rule3))]
("squirrel" "chases" "tiger" "+")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel does not chase the tiger.
("squirrel" "chases" "tiger" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The tiger does not need the cow.
Unknown
inv-rconc
[@3: The tiger needs the cow.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule1 <- FAIL)]]
("tiger" "needs" "cow" "-")
The cow is kind.
Unknown
rconc
[@3: The cow is kind.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule1 <- FAIL)]]
("cow" "is" "kind" "+")
The cow is not blue.
Unknown
inv-rconc
[@1: The cow is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "blue" "-")
The tiger is blue.
Unknown
rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "blue" "+")
The squirrel is not red.
Unknown
inv-random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "-")
The cow chases the tiger.
Unknown
random
[@0: The cow chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "tiger" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow chases the squirrel.[(triple1)] The squirrel is blue.[(triple2)] The tiger eats the cow.[(triple3)] @1: The squirrel is green.[(((triple2) -> rule4))] @2: The squirrel is kind.[(((((triple2) -> rule4)) -> rule5))] The squirrel needs the cow.[(((((triple2) -> rule4)) -> rule7))] @3: The squirrel does not chase the tiger.[(((((((triple2) -> rule4)) -> rule5)) -> rule3))]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple1
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple2
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple3
The squirrel is green.
("squirrel" "is" "green" "+")
((triple2) -> (rule4 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel does not chase the tiger.
("squirrel" "chases" "tiger" "-")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel does not chase the tiger.
("squirrel" "chases" "tiger" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3