The cow is nice. All nice, rough people are red. If someone is blue then they are rough. If someone is rough then they are blue. Rough people are red. If the cow is red then the cow is blue. All cold people are nice. If someone is red then they are rough. Nice people are red.
The cow is nice.
("cow" "is" "nice" "+")
All nice, rough people are red.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If someone is blue then they are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough then they are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
Rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If the cow is red then the cow is blue.
((("cow" "is" "red" "+")) -> ("cow" "is" "blue" "+"))
All cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is red then they are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
The cow is nice.
True
1
proof
[(triple1)]
("cow" "is" "nice" "+")
triple1
The cow is not nice.
False
1
inv-proof
[(triple1)]
("cow" "is" "nice" "-")
triple1
The cow is red.
True
2
proof
[(((triple1) -> rule8))]
("cow" "is" "red" "+")
((triple1) -> (rule8 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is not red.
False
2
inv-proof
[(((triple1) -> rule8))]
("cow" "is" "red" "-")
((triple1) -> (rule8 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is rough.
True
3
proof
[(((((triple1) -> rule8)) -> rule7) OR ((((((triple1) -> rule8)) -> rule5)) -> rule2))]
("cow" "is" "rough" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
((((((triple1) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is not rough.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule7) OR ((((((triple1) -> rule8)) -> rule5)) -> rule2))]
("cow" "is" "rough" "-")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
((((((triple1) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
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 cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow is nice.[(triple1)] @1: The cow is red.[(((triple1) -> rule8))] @2: The cow is blue.[(((((triple1) -> rule8)) -> rule5) OR ((((((triple1) -> rule8)) -> rule7)) -> rule3))] The cow is rough.[(((((triple1) -> rule8)) -> rule7) OR ((((((triple1) -> rule8)) -> rule5)) -> rule2))]
The cow is nice.
("cow" "is" "nice" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
((triple1) -> (rule8 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is rough.
("cow" "is" "rough" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
((((((triple1) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3