The cow is young. Big things are kind. Young things are red. If the cow is red then the cow is kind. If the cow is young and the cow is kind then the cow is big. If something is blue and big then it is young. If something is kind then it is red. If something is kind and young then it is red. If something is big then it is young.
The cow is young.
("cow" "is" "young" "+")
Big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If the cow is red then the cow is kind.
((("cow" "is" "red" "+")) -> ("cow" "is" "kind" "+"))
If the cow is young and the cow is kind then the cow is big.
((("cow" "is" "young" "+") ("cow" "is" "kind" "+")) -> ("cow" "is" "big" "+"))
If something is blue and big then it is young.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is kind then it is red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something is kind and young then it is red.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is big then it is young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
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 red.
True
2
proof
[(((triple1) -> rule2))]
("cow" "is" "red" "+")
((triple1) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is not red.
False
2
inv-proof
[(((triple1) -> rule2))]
("cow" "is" "red" "-")
((triple1) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is kind.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("cow" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is not kind.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("cow" "is" "kind" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is big.
True
5
proof
[(((triple1 ((((triple1) -> rule2)) -> rule3)) -> rule4))]
("cow" "is" "big" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is not big.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule2)) -> rule3)) -> rule4))]
("cow" "is" "big" "-")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
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 does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
@0: The cow is young.[(triple1)] @1: The cow is red.[(((triple1) -> rule2))] @2: The cow is kind.[(((((triple1) -> rule2)) -> rule3))] @3: The cow is big.[(((triple1 ((((triple1) -> rule2)) -> rule3)) -> rule4))]
The cow is young.
("cow" "is" "young" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
((triple1) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is big.
("cow" "is" "big" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3