The cow is young. If something is red then it is young. All kind, young things are red. If the cow is young and the cow is rough then the cow is red. If the cow is rough and the cow is young then the cow is nice. If something is red and rough then it is nice. All nice, red things are rough. If something is red and rough then it is young. If the cow is young then the cow is rough.
The cow is young.
("cow" "is" "young" "+")
If something is red then it is young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All kind, young things are red.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If the cow is young and the cow is rough then the cow is red.
((("cow" "is" "young" "+") ("cow" "is" "rough" "+")) -> ("cow" "is" "red" "+"))
If the cow is rough and the cow is young then the cow is nice.
((("cow" "is" "rough" "+") ("cow" "is" "young" "+")) -> ("cow" "is" "nice" "+"))
If something is red and rough then it is nice.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All nice, red things are rough.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is red and rough then it is young.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If the cow is young then the cow is rough.
((("cow" "is" "young" "+")) -> ("cow" "is" "rough" "+"))
The cow is young.
True
1
proof
[(triple1)]
("cow" "is" "young" "+")
triple1
The cow is not young.
False
1
inv-proof
[(triple1)]
("cow" "is" "young" "-")
triple1
The cow is rough.
True
2
proof
[(((triple1) -> rule8))]
("cow" "is" "rough" "+")
((triple1) -> (rule8 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is not rough.
False
2
inv-proof
[(((triple1) -> rule8))]
("cow" "is" "rough" "-")
((triple1) -> (rule8 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is nice.
True
4
proof
[(((((triple1) -> rule8) triple1) -> rule4) OR ((((triple1 ((triple1) -> rule8)) -> rule3) ((triple1) -> rule8)) -> rule5))]
("cow" "is" "nice" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule4 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule3 % int2)) ((triple1) -> (rule8 % int3))) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow is not red.
False
4
inv-proof
[(((triple1 ((triple1) -> rule8)) -> rule3))]
("cow" "is" "red" "-")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
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 young.[(triple1)] @1: The cow is rough.[(((triple1) -> rule8))] @2: The cow is nice.[(((((triple1) -> rule8) triple1) -> rule4) OR ((((triple1 ((triple1) -> rule8)) -> rule3) ((triple1) -> rule8)) -> rule5))] The cow is red.[(((triple1 ((triple1) -> rule8)) -> rule3))]
The cow is young.
("cow" "is" "young" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
((triple1) -> (rule8 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule4 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule3 % int2)) ((triple1) -> (rule8 % int3))) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow is red.
("cow" "is" "red" "+")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2