The cow is blue. All kind people are blue. If the cow is blue and the cow is kind then the cow is young. All blue people are kind. If the cow is blue and the cow is young then the cow is big. If someone is young and kind then they are big. Kind people are young.
The cow is blue.
("cow" "is" "blue" "+")
All kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If the cow is blue and the cow is kind then the cow is young.
((("cow" "is" "blue" "+") ("cow" "is" "kind" "+")) -> ("cow" "is" "young" "+"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If the cow is blue and the cow is young then the cow is big.
((("cow" "is" "blue" "+") ("cow" "is" "young" "+")) -> ("cow" "is" "big" "+"))
If someone is young and kind then they are big.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
The cow is blue.
True
1
proof
[(triple1)]
("cow" "is" "blue" "+")
triple1
The cow is not blue.
False
1
inv-proof
[(triple1)]
("cow" "is" "blue" "-")
triple1
The cow is kind.
True
2
proof
[(((triple1) -> rule3))]
("cow" "is" "kind" "+")
((triple1) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "is" "kind" "-")
((triple1) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "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 red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
@0: The cow is blue.[(triple1)] @1: The cow is kind.[(((triple1) -> rule3))] @2: The cow is young.[(((((triple1) -> rule3)) -> rule6) OR ((triple1 ((triple1) -> rule3)) -> rule2))] @3: The cow is big.[(((triple1 ((((triple1) -> rule3)) -> rule6)) -> rule4) OR ((triple1 ((triple1 ((triple1) -> rule3)) -> rule2)) -> rule4) OR ((((((triple1) -> rule3)) -> rule6) ((triple1) -> rule3)) -> rule5) OR ((((triple1 ((triple1) -> rule3)) -> rule2) ((triple1) -> rule3)) -> rule5))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
((triple1) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is young.
("cow" "is" "young" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is big.
("cow" "is" "big" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
((triple1 ((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2)) ((triple1) -> (rule3 % int3))) -> (rule5 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2)) ((triple1) -> (rule3 % int3))) -> (rule5 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3