The cow visits the tiger. The tiger is kind. The tiger visits the cow. If someone needs the cow then the cow is kind. If someone is kind then they need the cow. If someone is green and they eat the tiger then the tiger visits the cow.
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If someone needs the cow then the cow is kind.
((("someone" "needs" "cow" "+")) -> ("cow" "is" "kind" "+"))
If someone is kind then they need the cow.
((("someone" "is" "kind" "+")) -> ("someone" "needs" "cow" "+"))
If someone is green and they eat the tiger then the tiger visits the cow.
((("someone" "is" "green" "+") ("someone" "eats" "tiger" "+")) -> ("tiger" "visits" "cow" "+"))
The tiger is kind.
True
1
proof
[(triple2)]
("tiger" "is" "kind" "+")
triple2
The tiger is not kind.
False
1
inv-proof
[(triple2)]
("tiger" "is" "kind" "-")
triple2
The tiger needs the cow.
True
2
proof
[(((triple2) -> rule2))]
("tiger" "needs" "cow" "+")
((triple2) -> (rule2 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger does not need the cow.
False
2
inv-proof
[(((triple2) -> rule2))]
("tiger" "needs" "cow" "-")
((triple2) -> (rule2 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The cow is kind.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("cow" "is" "kind" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The cow is not kind.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("cow" "is" "kind" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The cow needs the cow.
True
4
proof
[(((((((triple2) -> rule2)) -> rule1)) -> rule2))]
("cow" "needs" "cow" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3
The cow does not need the cow.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule1)) -> rule2))]
("cow" "needs" "cow" "-")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3
The tiger is not blue.
Unknown
inv-random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "-")
The tiger eats the cow.
Unknown
random
[@0: The tiger eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "cow" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
@0: The cow visits the tiger.[(triple1)] The tiger is kind.[(triple2)] The tiger visits the cow.[(triple3)] @1: The tiger needs the cow.[(((triple2) -> rule2))] @2: The cow is kind.[(((((triple2) -> rule2)) -> rule1))] @3: The cow needs the cow.[(((((((triple2) -> rule2)) -> rule1)) -> rule2))]
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple1
The tiger is kind.
("tiger" "is" "kind" "+")
triple2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple3
The tiger needs the cow.
("tiger" "needs" "cow" "+")
((triple2) -> (rule2 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3