The cow is blue. All rough, blue things are green. Nice things are cold. Green, nice things are blue. All green things are rough. Nice things are blue. Rough things are nice. If something is blue then it is green. Green, blue things are nice.
The cow is blue.
("cow" "is" "blue" "+")
All rough, blue things are green.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Green, nice things are blue.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
All green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Green, blue things are nice.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
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 green.
True
2
proof
[(((triple1) -> rule7))]
("cow" "is" "green" "+")
((triple1) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is not green.
False
2
inv-proof
[(((triple1) -> rule7))]
("cow" "is" "green" "-")
((triple1) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is nice.
True
4
proof
[(((((triple1) -> rule7) triple1) -> rule8) OR ((((((triple1) -> rule7)) -> rule4)) -> rule6))]
("cow" "is" "nice" "+")
((((triple1) -> (rule7 % int2)) triple1) -> (rule8 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow is not rough.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule4))]
("cow" "is" "rough" "-")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is cold.
True
5
proof
[(((((((triple1) -> rule7) triple1) -> rule8)) -> rule2) OR ((((((((triple1) -> rule7)) -> rule4)) -> rule6)) -> rule2))]
("cow" "is" "cold" "+")
((((((triple1) -> (rule7 % int3)) triple1) -> (rule8 % int2))) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
((((((((triple1) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow is green.
("cow" "is" "green" "+")
int4
The cow is not cold.
False
5
inv-proof
[(((((((triple1) -> rule7) triple1) -> rule8)) -> rule2) OR ((((((((triple1) -> rule7)) -> rule4)) -> rule6)) -> rule2))]
("cow" "is" "cold" "-")
((((((triple1) -> (rule7 % int3)) triple1) -> (rule8 % int2))) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
((((((((triple1) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow is green.
("cow" "is" "green" "+")
int4
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The cow is blue.[(triple1)] @1: The cow is green.[(((triple1) -> rule7))] @2: The cow is nice.[(((((triple1) -> rule7) triple1) -> rule8) OR ((((((triple1) -> rule7)) -> rule4)) -> rule6))] The cow is rough.[(((((triple1) -> rule7)) -> rule4))] @3: The cow is cold.[(((((((triple1) -> rule7) triple1) -> rule8)) -> rule2) OR ((((((((triple1) -> rule7)) -> rule4)) -> rule6)) -> rule2))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
((triple1) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
((((triple1) -> (rule7 % int2)) triple1) -> (rule8 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow is rough.
("cow" "is" "rough" "+")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
((((((triple1) -> (rule7 % int3)) triple1) -> (rule8 % int2))) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
((((((((triple1) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow is green.
("cow" "is" "green" "+")
int4