The cat is rough. The cat does not see the tiger. The cow sees the cat. The cow sees the tiger. The squirrel eats the tiger. The squirrel is kind. The tiger sees the squirrel. If the cow chases the squirrel and the tiger does not see the cow then the tiger is red. Big people are rough. If someone chases the cat then the cat does not chase the tiger. Kind people are big. If the cat is red then the cat eats the tiger. If someone sees the cat then the cat is red. If someone is kind and they chase the tiger then the tiger does not chase the squirrel. If someone sees the squirrel and the squirrel is rough then they are kind. If someone eats the cow and they are not red then the cow does not eat the squirrel.
The cat is rough.
("cat" "is" "rough" "+")
The cat does not see the tiger.
("cat" "sees" "tiger" "-")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If the cow chases the squirrel and the tiger does not see the cow then the tiger is red.
((("cow" "chases" "squirrel" "+") ("tiger" "sees" "cow" "~")) -> ("tiger" "is" "red" "+"))
Big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If someone chases the cat then the cat does not chase the tiger.
((("someone" "chases" "cat" "+")) -> ("cat" "chases" "tiger" "-"))
Kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If the cat is red then the cat eats the tiger.
((("cat" "is" "red" "+")) -> ("cat" "eats" "tiger" "+"))
If someone sees the cat then the cat is red.
((("someone" "sees" "cat" "+")) -> ("cat" "is" "red" "+"))
If someone is kind and they chase the tiger then the tiger does not chase the squirrel.
((("someone" "is" "kind" "+") ("someone" "chases" "tiger" "+")) -> ("tiger" "chases" "squirrel" "-"))
If someone sees the squirrel and the squirrel is rough then they are kind.
((("someone" "sees" "squirrel" "+") ("squirrel" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone eats the cow and they are not red then the cow does not eat the squirrel.
((("someone" "eats" "cow" "+") ("someone" "is" "red" "~")) -> ("cow" "eats" "squirrel" "-"))
The cat does not see the tiger.
True
1
proof
[(triple2)]
("cat" "sees" "tiger" "-")
triple2
The cat is not rough.
False
1
inv-proof
[(triple1)]
("cat" "is" "rough" "-")
triple1
The cat is red.
True
2
proof
[(((triple3) -> rule6))]
("cat" "is" "red" "+")
((triple3) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is not red.
False
2
inv-proof
[(((triple3) -> rule6))]
("cat" "is" "red" "-")
((triple3) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The squirrel is rough.
True
3
proof
[(((((triple6) -> rule4)) -> rule2))]
("squirrel" "is" "rough" "+")
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The cat does not eat the tiger.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule5))]
("cat" "eats" "tiger" "-")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The tiger is kind.
True
5
proof
[(((triple7 ((((triple6) -> rule4)) -> rule2)) -> rule8))]
("tiger" "is" "kind" "+")
((triple7 ((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The tiger is not kind.
False
5
inv-proof
[(((triple7 ((((triple6) -> rule4)) -> rule2)) -> rule8))]
("tiger" "is" "kind" "-")
((triple7 ((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The tiger is big.
True
6
proof
[(((((triple7 ((((triple6) -> rule4)) -> rule2)) -> rule8)) -> rule4))]
("tiger" "is" "big" "+")
((((triple7 ((((triple6) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel is big.
("squirrel" "is" "big" "+")
int4
The tiger is not big.
False
6
inv-proof
[(((((triple7 ((((triple6) -> rule4)) -> rule2)) -> rule8)) -> rule4))]
("tiger" "is" "big" "-")
((((triple7 ((((triple6) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel is big.
("squirrel" "is" "big" "+")
int4
The tiger is rough.
True
7
proof
[(((((((triple7 ((((triple6) -> rule4)) -> rule2)) -> rule8)) -> rule4)) -> rule2))]
("tiger" "is" "rough" "+")
((((((triple7 ((((triple6) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4
The squirrel is big.
("squirrel" "is" "big" "+")
int5
The tiger is not rough.
False
7
inv-proof
[(((((((triple7 ((((triple6) -> rule4)) -> rule2)) -> rule8)) -> rule4)) -> rule2))]
("tiger" "is" "rough" "-")
((((((triple7 ((((triple6) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4
The squirrel is big.
("squirrel" "is" "big" "+")
int5
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "red" "-")
The cat is big.
Unknown
rconc
[@2: The cat is big.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("cat" "is" "big" "+")
The cow is not rough.
Unknown
inv-rconc
[@3: The cow is rough.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule8 <- FAIL)]]
("cow" "is" "rough" "-")
The cow is kind.
Unknown
rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "is" "kind" "+")
The cow is not big.
Unknown
inv-rconc
[@2: The cow is big.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("cow" "is" "big" "-")
The cat is kind.
Unknown
rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "kind" "+")
The tiger does not chase the cow.
Unknown
inv-random
[@0: The tiger chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cow" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel chases the tiger.
Unknown
random
[@0: The squirrel chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "tiger" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
@0: The cat does not see the tiger.[(triple2)] The cat is rough.[(triple1)] The cow sees the cat.[(triple3)] The cow sees the tiger.[(triple4)] The squirrel eats the tiger.[(triple5)] The squirrel is kind.[(triple6)] The tiger sees the squirrel.[(triple7)] @1: The cat is red.[(((triple3) -> rule6))] The squirrel is big.[(((triple6) -> rule4))] @2: The cat eats the tiger.[(((((triple3) -> rule6)) -> rule5))] The squirrel is rough.[(((((triple6) -> rule4)) -> rule2))] @3: The tiger is kind.[(((triple7 ((((triple6) -> rule4)) -> rule2)) -> rule8))] @4: The tiger is big.[(((((triple7 ((((triple6) -> rule4)) -> rule2)) -> rule8)) -> rule4))] @5: The tiger is rough.[(((((((triple7 ((((triple6) -> rule4)) -> rule2)) -> rule8)) -> rule4)) -> rule2))]
The cat does not see the tiger.
("cat" "sees" "tiger" "-")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple1
The cow sees the cat.
("cow" "sees" "cat" "+")
triple3
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple4
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple5
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple6
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple7
The cat is red.
("cat" "is" "red" "+")
((triple3) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((triple6) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
((triple7 ((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
((((triple7 ((((triple6) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel is big.
("squirrel" "is" "big" "+")
int4
The tiger is rough.
("tiger" "is" "rough" "+")
((((((triple7 ((((triple6) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4
The squirrel is big.
("squirrel" "is" "big" "+")
int5