The cow is kind. If something is kind and red then it is cold. Kind, big things are blue. If something is big then it is kind. If the cow is kind then the cow is red. Kind things are blue. If the cow is blue and the cow is cold then the cow is kind. If something is kind then it is blue. All kind, cold things are big.
The cow is kind.
("cow" "is" "kind" "+")
If something is kind and red then it is cold.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Kind, big things are blue.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If the cow is kind then the cow is red.
((("cow" "is" "kind" "+")) -> ("cow" "is" "red" "+"))
Kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If the cow is blue and the cow is cold then the cow is kind.
((("cow" "is" "blue" "+") ("cow" "is" "cold" "+")) -> ("cow" "is" "kind" "+"))
If something is kind then it is blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
All kind, cold things are big.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
The cow is kind.
True
1
proof
[(triple1)]
("cow" "is" "kind" "+")
triple1
The cow is not kind.
False
1
inv-proof
[(triple1)]
("cow" "is" "kind" "-")
triple1
The cow is blue.
True
2
proof
[(((triple1) -> rule5) OR ((triple1) -> rule7) OR ((triple1 ((triple1 ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule8)) -> rule2))]
("cow" "is" "blue" "+")
((triple1) -> (rule5 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple1) -> (rule7 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple1 ((triple1 ((triple1 ((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The cow is not blue.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple1) -> rule7) OR ((triple1 ((triple1 ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule8)) -> rule2))]
("cow" "is" "blue" "-")
((triple1) -> (rule5 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple1) -> (rule7 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple1 ((triple1 ((triple1 ((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The cow is cold.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule1))]
("cow" "is" "cold" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is not cold.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule1))]
("cow" "is" "cold" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
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 eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow is kind.[(triple1)] @1: The cow is blue.[(((triple1) -> rule5) OR ((triple1) -> rule7) OR ((triple1 ((triple1 ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule8)) -> rule2))] The cow is red.[(((triple1) -> rule4))] @2: The cow is cold.[(((triple1 ((triple1) -> rule4)) -> rule1))] @3: The cow is big.[(((triple1 ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule8))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
((triple1) -> (rule5 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple1) -> (rule7 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple1 ((triple1 ((triple1 ((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The cow is red.
("cow" "is" "red" "+")
((triple1) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is big.
("cow" "is" "big" "+")
((triple1 ((triple1 ((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3