The cow is rough. The cow does not need the squirrel. The cow needs the tiger. The cow sees the tiger. The squirrel chases the tiger. The squirrel needs the cow. The squirrel needs the tiger. The squirrel sees the tiger. The tiger chases the cow. The tiger chases the squirrel. The tiger is cold. The tiger is kind. The tiger needs the cow. The tiger needs the squirrel. The tiger sees the cow. The tiger sees the squirrel. If someone is rough and cold then they do not chase the tiger. If someone is round then they do not chase the tiger. If the tiger is young and the tiger chases the cow then the cow is round. If the tiger is round and the tiger does not see the cow then the cow does not chase the squirrel. If someone needs the tiger then they are kind. If someone is kind then they are young.
The cow is rough.
("cow" "is" "rough" "+")
The cow does not need the squirrel.
("cow" "needs" "squirrel" "-")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If someone is rough and cold then they do not chase the tiger.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "chases" "tiger" "-"))
If someone is round then they do not chase the tiger.
((("someone" "is" "round" "+")) -> ("someone" "chases" "tiger" "-"))
If the tiger is young and the tiger chases the cow then the cow is round.
((("tiger" "is" "young" "+") ("tiger" "chases" "cow" "+")) -> ("cow" "is" "round" "+"))
If the tiger is round and the tiger does not see the cow then the cow does not chase the squirrel.
((("tiger" "is" "round" "+") ("tiger" "sees" "cow" "~")) -> ("cow" "chases" "squirrel" "-"))
If someone needs the tiger then they are kind.
((("someone" "needs" "tiger" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind then they are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
The tiger needs the squirrel.
True
1
proof
[(triple14)]
("tiger" "needs" "squirrel" "+")
triple14
The cow does not need the tiger.
False
1
inv-proof
[(triple3)]
("cow" "needs" "tiger" "-")
triple3
The squirrel is kind.
True
2
proof
[(((triple7) -> rule5))]
("squirrel" "is" "kind" "+")
((triple7) -> (rule5 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is not kind.
False
2
inv-proof
[(((triple7) -> rule5))]
("squirrel" "is" "kind" "-")
((triple7) -> (rule5 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The cow is young.
True
3
proof
[(((((triple3) -> rule5)) -> rule6))]
("cow" "is" "young" "+")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is not young.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule6))]
("cow" "is" "young" "-")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow does not chase the tiger.
True
5
proof
[(((((((triple12) -> rule6) triple9) -> rule3)) -> rule2))]
("cow" "chases" "tiger" "-")
((((((triple12) -> (rule6 % int3)) triple9) -> (rule3 % int2))) -> (rule2 % int1))
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The cow chases the tiger.
False
5
inv-proof
[(((((((triple12) -> rule6) triple9) -> rule3)) -> rule2))]
("cow" "chases" "tiger" "+")
((((((triple12) -> (rule6 % int3)) triple9) -> (rule3 % int2))) -> (rule2 % int1))
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The cow does not see the squirrel.
Unknown
inv-random
[@0: The cow sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "squirrel" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The squirrel sees the cow.
Unknown
random
[@0: The squirrel sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "cow" "+")
@0: The cow does not need the squirrel.[(triple2)] The cow is rough.[(triple1)] The cow needs the tiger.[(triple3)] The cow sees the tiger.[(triple4)] The squirrel chases the tiger.[(triple5)] The squirrel needs the cow.[(triple6)] The squirrel needs the tiger.[(triple7)] The squirrel sees the tiger.[(triple8)] The tiger chases the cow.[(triple9)] The tiger chases the squirrel.[(triple10)] The tiger is cold.[(triple11)] The tiger is kind.[(triple12)] The tiger needs the cow.[(triple13)] The tiger needs the squirrel.[(triple14)] The tiger sees the cow.[(triple15)] The tiger sees the squirrel.[(triple16)] @1: The cow is kind.[(((triple3) -> rule5))] The squirrel is kind.[(((triple7) -> rule5))] The tiger is young.[(((triple12) -> rule6))] @2: The cow is round.[(((((triple12) -> rule6) triple9) -> rule3))] The cow is young.[(((((triple3) -> rule5)) -> rule6))] The squirrel is young.[(((((triple7) -> rule5)) -> rule6))] @3: The cow does not chase the tiger.[(((((((triple12) -> rule6) triple9) -> rule3)) -> rule2))]
The cow does not need the squirrel.
("cow" "needs" "squirrel" "-")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple3
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple4
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple5
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple6
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple7
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple8
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple9
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger is kind.
("tiger" "is" "kind" "+")
triple12
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple13
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple14
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple15
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple16
The cow is kind.
("cow" "is" "kind" "+")
((triple3) -> (rule5 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple7) -> (rule5 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
((triple12) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The cow is round.
("cow" "is" "round" "+")
((((triple12) -> (rule6 % int2)) triple9) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The cow is young.
("cow" "is" "young" "+")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
((((triple7) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
((((((triple12) -> (rule6 % int3)) triple9) -> (rule3 % int2))) -> (rule2 % int1))
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3