The cow is rough. Rough people are red. If the cow is rough then the cow is blue. If the cow is rough and the cow is green then the cow is not nice. If someone is blue and red then they are green. If someone is nice and not blue then they are green. Nice people are green.
The cow is rough.
("cow" "is" "rough" "+")
Rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If the cow is rough then the cow is blue.
((("cow" "is" "rough" "+")) -> ("cow" "is" "blue" "+"))
If the cow is rough and the cow is green then the cow is not nice.
((("cow" "is" "rough" "+") ("cow" "is" "green" "+")) -> ("cow" "is" "nice" "-"))
If someone is blue and red then they are green.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is nice and not blue then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "green" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
The cow is rough.
True
1
proof
[(triple1)]
("cow" "is" "rough" "+")
triple1
The cow is not rough.
False
1
inv-proof
[(triple1)]
("cow" "is" "rough" "-")
triple1
The cow is blue.
True
2
proof
[(((triple1) -> rule2))]
("cow" "is" "blue" "+")
((triple1) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is not blue.
False
2
inv-proof
[(((triple1) -> rule2))]
("cow" "is" "blue" "-")
((triple1) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
True
5
proof
[(((((triple1) -> rule2) ((triple1) -> rule1)) -> rule4))]
("cow" "is" "green" "+")
((((triple1) -> (rule2 % int3)) ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The cow is not green.
False
5
inv-proof
[(((((triple1) -> rule2) ((triple1) -> rule1)) -> rule4))]
("cow" "is" "green" "-")
((((triple1) -> (rule2 % int3)) ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The cow is not nice.
True
7
proof
[(((triple1 ((((triple1) -> rule2) ((triple1) -> rule1)) -> rule4)) -> rule3))]
("cow" "is" "nice" "-")
((triple1 ((((triple1) -> (rule2 % int4)) ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
int4
The cow is nice.
False
7
inv-proof
[(((triple1 ((((triple1) -> rule2) ((triple1) -> rule1)) -> rule4)) -> rule3))]
("cow" "is" "nice" "+")
((triple1 ((((triple1) -> (rule2 % int4)) ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
int4
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow is rough.[(triple1)] @1: The cow is blue.[(((triple1) -> rule2))] The cow is red.[(((triple1) -> rule1))] @2: The cow is green.[(((((triple1) -> rule2) ((triple1) -> rule1)) -> rule4))] @3: The cow is not nice.[(((triple1 ((((triple1) -> rule2) ((triple1) -> rule1)) -> rule4)) -> rule3))]
The cow is rough.
("cow" "is" "rough" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
((triple1) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is red.
("cow" "is" "red" "+")
((triple1) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is green.
("cow" "is" "green" "+")
((((triple1) -> (rule2 % int3)) ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The cow is not nice.
("cow" "is" "nice" "-")
((triple1 ((((triple1) -> (rule2 % int4)) ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
int4