The cow is green. The cow is kind. The cow is rough. Rough, young people are nice. All young, nice people are green. If the cow is rough and the cow is nice then the cow is young. All nice, young people are kind. Green people are nice. If someone is young and nice then they are green.
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is rough.
("cow" "is" "rough" "+")
Rough, young people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
All young, nice people are green.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If the cow is rough and the cow is nice then the cow is young.
((("cow" "is" "rough" "+") ("cow" "is" "nice" "+")) -> ("cow" "is" "young" "+"))
All nice, young people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone is young and nice then they are green.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
The cow is rough.
True
1
proof
[(triple3)]
("cow" "is" "rough" "+")
triple3
The cow is not kind.
False
1
inv-proof
[(triple2 OR ((((triple1) -> rule5) ((triple3 ((triple1) -> rule5)) -> rule3)) -> rule4))]
("cow" "is" "kind" "-")
triple2
((((triple1) -> (rule5 % int3)) ((triple3 ((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The cow is nice.
True
2
proof
[(((triple1) -> rule5))]
("cow" "is" "nice" "+")
((triple1) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is not nice.
False
2
inv-proof
[(((triple1) -> rule5))]
("cow" "is" "nice" "-")
((triple1) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is young.
True
4
proof
[(((triple3 ((triple1) -> rule5)) -> rule3))]
("cow" "is" "young" "+")
((triple3 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is not young.
False
4
inv-proof
[(((triple3 ((triple1) -> rule5)) -> rule3))]
("cow" "is" "young" "-")
((triple3 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
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 likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The cow is green.[(triple1)] The cow is kind.[(triple2 OR ((((triple1) -> rule5) ((triple3 ((triple1) -> rule5)) -> rule3)) -> rule4))] The cow is rough.[(triple3)] @1: The cow is nice.[(((triple1) -> rule5))] @2: The cow is young.[(((triple3 ((triple1) -> rule5)) -> rule3))]
The cow is green.
("cow" "is" "green" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple2
((((triple1) -> (rule5 % int3)) ((triple3 ((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The cow is rough.
("cow" "is" "rough" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
((triple1) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is young.
("cow" "is" "young" "+")
((triple3 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2