The cow is red. All young things are rough. If something is red then it is rough. If something is red and rough then it is not young. Rough things are red. All cold things are green. If something is red and not young then it is cold. Green things are cold. If the cow is cold and the cow is rough then the cow is green.
The cow is red.
("cow" "is" "red" "+")
All young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is red and rough then it is not young.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "-"))
Rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is red and not young then it is cold.
((("something" "is" "red" "+") ("something" "is" "young" "~")) -> ("something" "is" "cold" "+"))
Green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If the cow is cold and the cow is rough then the cow is green.
((("cow" "is" "cold" "+") ("cow" "is" "rough" "+")) -> ("cow" "is" "green" "+"))
The cow is red.
True
1
proof
[(triple1)]
("cow" "is" "red" "+")
triple1
The cow is not red.
False
1
inv-proof
[(triple1)]
("cow" "is" "red" "-")
triple1
The cow is rough.
True
2
proof
[(((triple1) -> rule2))]
("cow" "is" "rough" "+")
((triple1) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("cow" "is" "rough" "-")
((triple1) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is not young.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("cow" "is" "young" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cow is not young.
("cow" "is" "young" "-")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is young.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("cow" "is" "young" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cow is not young.
("cow" "is" "young" "-")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is cold.
True
6
proof
[(((triple1 ((triple1 ((triple1) -> rule2)) -> rule3)) -> rule6))]
("cow" "is" "cold" "+")
((triple1 ((triple1 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is not young.
("cow" "is" "young" "-")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow is not cold.
False
6
inv-proof
[(((triple1 ((triple1 ((triple1) -> rule2)) -> rule3)) -> rule6))]
("cow" "is" "cold" "-")
((triple1 ((triple1 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is not young.
("cow" "is" "young" "-")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
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 visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cow is red.[(triple1)] @1: The cow is rough.[(((triple1) -> rule2))] @2: The cow is not young.[(((triple1 ((triple1) -> rule2)) -> rule3))] @3: The cow is cold.[(((triple1 ((triple1 ((triple1) -> rule2)) -> rule3)) -> rule6))] @4: The cow is green.[(((((triple1 ((triple1 ((triple1) -> rule2)) -> rule3)) -> rule6)) -> rule5) OR ((((triple1 ((triple1 ((triple1) -> rule2)) -> rule3)) -> rule6) ((triple1) -> rule2)) -> rule8))]
The cow is red.
("cow" "is" "red" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
((triple1) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is not young.
("cow" "is" "young" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cow is not young.
("cow" "is" "young" "-")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
((triple1 ((triple1 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is not young.
("cow" "is" "young" "-")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow is green.
("cow" "is" "green" "+")
((((triple1 ((triple1 ((triple1) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is not young.
("cow" "is" "young" "-")
int3
The cow is rough.
("cow" "is" "rough" "+")
int4
((((triple1 ((triple1 ((triple1) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) ((triple1) -> (rule2 % int4))) -> (rule8 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is not young.
("cow" "is" "young" "-")
int3
The cow is rough.
("cow" "is" "rough" "+")
int4