The cow is green. The cow is kind. The cow is not nice. The cow is red. The cow is young. Red people are kind. All kind people are red. Red people are young. If someone is green then they are young. If someone is green and nice then they are young. If someone is red and not kind then they are young. If someone is nice and red then they are green. Kind, young people are not nice.
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is not nice.
("cow" "is" "nice" "-")
The cow is red.
("cow" "is" "red" "+")
The cow is young.
("cow" "is" "young" "+")
Red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
Red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is green then they are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is green and nice then they are young.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If someone is red and not kind then they are young.
((("someone" "is" "red" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "young" "+"))
If someone is nice and red then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Kind, young people are not nice.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "-"))
The cow is green.
True
1
proof
[(triple1)]
("cow" "is" "green" "+")
triple1
The cow is nice.
False
1
inv-proof
[(triple3 OR ((triple2 triple5) -> rule8) OR ((triple2 ((triple1) -> rule4)) -> rule8) OR ((triple2 ((triple4) -> rule3)) -> rule8) OR ((((triple4) -> rule1) triple5) -> rule8) OR ((((triple4) -> rule1) ((triple1) -> rule4)) -> rule8) OR ((((triple4) -> rule1) ((triple4) -> rule3)) -> rule8) OR ((triple2 ((((triple2) -> rule2)) -> rule3)) -> rule8) OR ((((triple4) -> rule1) ((((triple2) -> rule2)) -> rule3)) -> rule8))]
("cow" "is" "nice" "+")
triple3
((triple2 triple5) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
((triple2 ((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is young.
("cow" "is" "young" "+")
int2
((triple2 ((triple4) -> (rule3 % int2))) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is young.
("cow" "is" "young" "+")
int2
((((triple4) -> (rule1 % int2)) triple5) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
((((triple4) -> (rule1 % int3)) ((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
((((triple4) -> (rule1 % int3)) ((triple4) -> (rule3 % int2))) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
((((triple4) -> (rule1 % int4)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
int4
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 chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow is green.[(triple1)] The cow is kind.[(triple2 OR ((triple4) -> rule1))] The cow is not nice.[(triple3 OR ((triple2 triple5) -> rule8) OR ((triple2 ((triple1) -> rule4)) -> rule8) OR ((triple2 ((triple4) -> rule3)) -> rule8) OR ((((triple4) -> rule1) triple5) -> rule8) OR ((((triple4) -> rule1) ((triple1) -> rule4)) -> rule8) OR ((((triple4) -> rule1) ((triple4) -> rule3)) -> rule8) OR ((triple2 ((((triple2) -> rule2)) -> rule3)) -> rule8) OR ((((triple4) -> rule1) ((((triple2) -> rule2)) -> rule3)) -> rule8))] The cow is red.[(triple4 OR ((triple2) -> rule2))] The cow is young.[(triple5 OR ((triple1) -> rule4) OR ((triple4) -> rule3) OR ((((triple2) -> rule2)) -> rule3))]
The cow is green.
("cow" "is" "green" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple2
((triple4) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is not nice.
("cow" "is" "nice" "-")
triple3
((triple2 triple5) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
((triple2 ((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is young.
("cow" "is" "young" "+")
int2
((triple2 ((triple4) -> (rule3 % int2))) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is young.
("cow" "is" "young" "+")
int2
((((triple4) -> (rule1 % int2)) triple5) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
((((triple4) -> (rule1 % int3)) ((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
((((triple4) -> (rule1 % int3)) ((triple4) -> (rule3 % int2))) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
((((triple4) -> (rule1 % int4)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
int4
The cow is red.
("cow" "is" "red" "+")
triple4
((triple2) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is young.
("cow" "is" "young" "+")
triple5
((triple1) -> (rule4 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((triple4) -> (rule3 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2