The cat chases the tiger. The cat is cold. The cat is green. The squirrel is cold. The squirrel is green. The squirrel is rough. The squirrel needs the tiger. The tiger chases the squirrel. The tiger needs the cat. The tiger does not need the squirrel. If someone eats the squirrel then the squirrel is not rough. If someone needs the tiger then the tiger eats the cat. If someone eats the squirrel then they need the tiger. If someone chases the cat then the cat is not rough. If someone eats the tiger then the tiger chases the squirrel. If someone eats the squirrel and they eat the cat then the squirrel needs the tiger. If someone is cold then they chase the cat. If someone chases the cat and the cat is not rough then the cat is not kind.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is green.
("cat" "is" "green" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
If someone eats the squirrel then the squirrel is not rough.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "is" "rough" "-"))
If someone needs the tiger then the tiger eats the cat.
((("someone" "needs" "tiger" "+")) -> ("tiger" "eats" "cat" "+"))
If someone eats the squirrel then they need the tiger.
((("someone" "eats" "squirrel" "+")) -> ("someone" "needs" "tiger" "+"))
If someone chases the cat then the cat is not rough.
((("someone" "chases" "cat" "+")) -> ("cat" "is" "rough" "-"))
If someone eats the tiger then the tiger chases the squirrel.
((("someone" "eats" "tiger" "+")) -> ("tiger" "chases" "squirrel" "+"))
If someone eats the squirrel and they eat the cat then the squirrel needs the tiger.
((("someone" "eats" "squirrel" "+") ("someone" "eats" "cat" "+")) -> ("squirrel" "needs" "tiger" "+"))
If someone is cold then they chase the cat.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the cat and the cat is not rough then the cat is not kind.
((("someone" "chases" "cat" "+") ("cat" "is" "rough" "~")) -> ("cat" "is" "kind" "-"))
The cat is green.
True
1
proof
[(triple3)]
("cat" "is" "green" "+")
triple3
The squirrel is not cold.
False
1
inv-proof
[(triple4)]
("squirrel" "is" "cold" "-")
triple4
The cat chases the cat.
True
2
proof
[(((triple2) -> rule7))]
("cat" "chases" "cat" "+")
((triple2) -> (rule7 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The squirrel does not chase the cat.
False
2
inv-proof
[(((triple4) -> rule7))]
("squirrel" "chases" "cat" "-")
((triple4) -> (rule7 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The cat is not rough.
True
3
proof
[(((((triple2) -> rule7)) -> rule4) OR ((((triple4) -> rule7)) -> rule4))]
("cat" "is" "rough" "-")
((((triple2) -> (rule7 % int2))) -> (rule4 % int1))
The cat is not rough.
("cat" "is" "rough" "-")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
((((triple4) -> (rule7 % int2))) -> (rule4 % int1))
The cat is not rough.
("cat" "is" "rough" "-")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
The cat is rough.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule4) OR ((((triple4) -> rule7)) -> rule4))]
("cat" "is" "rough" "+")
((((triple2) -> (rule7 % int2))) -> (rule4 % int1))
The cat is not rough.
("cat" "is" "rough" "-")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
((((triple4) -> (rule7 % int2))) -> (rule4 % int1))
The cat is not rough.
("cat" "is" "rough" "-")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
The cat is not kind.
True
6
proof
[(((((triple2) -> rule7) ((((triple2) -> rule7)) -> rule4)) -> rule8) OR ((((triple2) -> rule7) ((((triple4) -> rule7)) -> rule4)) -> rule8) OR ((((triple4) -> rule7) ((((triple2) -> rule7)) -> rule4)) -> rule8) OR ((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule4)) -> rule8))]
("cat" "is" "kind" "-")
((((triple2) -> (rule7 % int3)) ((((triple2) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is not rough.
("cat" "is" "rough" "-")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
((((triple2) -> (rule7 % int4)) ((((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is not rough.
("cat" "is" "rough" "-")
int2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int3
The cat chases the cat.
("cat" "chases" "cat" "+")
int4
((((triple4) -> (rule7 % int4)) ((((triple2) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is not rough.
("cat" "is" "rough" "-")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int4
((((triple4) -> (rule7 % int3)) ((((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is not rough.
("cat" "is" "rough" "-")
int2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int3
The cat is kind.
False
6
inv-proof
[(((((triple2) -> rule7) ((((triple2) -> rule7)) -> rule4)) -> rule8) OR ((((triple2) -> rule7) ((((triple4) -> rule7)) -> rule4)) -> rule8) OR ((((triple4) -> rule7) ((((triple2) -> rule7)) -> rule4)) -> rule8) OR ((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule4)) -> rule8))]
("cat" "is" "kind" "+")
((((triple2) -> (rule7 % int3)) ((((triple2) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is not rough.
("cat" "is" "rough" "-")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
((((triple2) -> (rule7 % int4)) ((((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is not rough.
("cat" "is" "rough" "-")
int2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int3
The cat chases the cat.
("cat" "chases" "cat" "+")
int4
((((triple4) -> (rule7 % int4)) ((((triple2) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is not rough.
("cat" "is" "rough" "-")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int4
((((triple4) -> (rule7 % int3)) ((((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is not rough.
("cat" "is" "rough" "-")
int2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int3
The cat does not need the tiger.
Unknown
inv-rconc
[@1: The cat needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "needs" "tiger" "-")
The tiger chases the cat.
Unknown
rconc
[@1: The tiger chases the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "chases" "cat" "+")
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The squirrel does not chase the squirrel.
Unknown
inv-random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The cat does not eat the squirrel.
Unknown
inv-random
[@0: The cat eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "squirrel" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat chases the tiger.[(triple1)] The cat is cold.[(triple2)] The cat is green.[(triple3)] The squirrel is cold.[(triple4)] The squirrel is green.[(triple5)] The squirrel is rough.[(triple6)] The squirrel needs the tiger.[(triple7)] The tiger chases the squirrel.[(triple8)] The tiger does not need the squirrel.[(triple10)] The tiger needs the cat.[(triple9)] @1: The cat chases the cat.[(((triple2) -> rule7))] The squirrel chases the cat.[(((triple4) -> rule7))] The tiger eats the cat.[(((triple7) -> rule2))] @2: The cat is not rough.[(((((triple2) -> rule7)) -> rule4) OR ((((triple4) -> rule7)) -> rule4))] @3: The cat is not kind.[(((((triple2) -> rule7) ((((triple2) -> rule7)) -> rule4)) -> rule8) OR ((((triple2) -> rule7) ((((triple4) -> rule7)) -> rule4)) -> rule8) OR ((((triple4) -> rule7) ((((triple2) -> rule7)) -> rule4)) -> rule8) OR ((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule4)) -> rule8))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple4
The squirrel is green.
("squirrel" "is" "green" "+")
triple5
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple6
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple7
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple8
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
triple10
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple9
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple2) -> (rule7 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
((triple4) -> (rule7 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
((triple7) -> (rule2 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The cat is not rough.
("cat" "is" "rough" "-")
((((triple2) -> (rule7 % int2))) -> (rule4 % int1))
The cat is not rough.
("cat" "is" "rough" "-")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
((((triple4) -> (rule7 % int2))) -> (rule4 % int1))
The cat is not rough.
("cat" "is" "rough" "-")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
The cat is not kind.
("cat" "is" "kind" "-")
((((triple2) -> (rule7 % int3)) ((((triple2) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is not rough.
("cat" "is" "rough" "-")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
((((triple2) -> (rule7 % int4)) ((((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is not rough.
("cat" "is" "rough" "-")
int2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int3
The cat chases the cat.
("cat" "chases" "cat" "+")
int4
((((triple4) -> (rule7 % int4)) ((((triple2) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is not rough.
("cat" "is" "rough" "-")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int4
((((triple4) -> (rule7 % int3)) ((((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is not rough.
("cat" "is" "rough" "-")
int2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int3