The cow is rough. If the cow is green then the cow is blue. All blue, rough things are not big. If the cow is rough then the cow is green. All green things are blue. If the cow is blue and the cow is not green then the cow is big. Rough, big things are young.
The cow is rough.
("cow" "is" "rough" "+")
If the cow is green then the cow is blue.
((("cow" "is" "green" "+")) -> ("cow" "is" "blue" "+"))
All blue, rough things are not big.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "-"))
If the cow is rough then the cow is green.
((("cow" "is" "rough" "+")) -> ("cow" "is" "green" "+"))
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If the cow is blue and the cow is not green then the cow is big.
((("cow" "is" "blue" "+") ("cow" "is" "green" "~")) -> ("cow" "is" "big" "+"))
Rough, big things are young.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
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 green.
True
2
proof
[(((triple1) -> rule3))]
("cow" "is" "green" "+")
((triple1) -> (rule3 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is not green.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "is" "green" "-")
((triple1) -> (rule3 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is blue.
True
3
proof
[(((((triple1) -> rule3)) -> rule1) OR ((((triple1) -> rule3)) -> rule4))]
("cow" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not blue.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1) OR ((((triple1) -> rule3)) -> rule4))]
("cow" "is" "blue" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not big.
True
5
proof
[(((((((triple1) -> rule3)) -> rule1) triple1) -> rule2) OR ((((((triple1) -> rule3)) -> rule4) triple1) -> rule2))]
("cow" "is" "big" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The cow is not big.
("cow" "is" "big" "-")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2)) triple1) -> (rule2 % int1))
The cow is not big.
("cow" "is" "big" "-")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow is big.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule1) triple1) -> rule2) OR ((((((triple1) -> rule3)) -> rule4) triple1) -> rule2))]
("cow" "is" "big" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The cow is not big.
("cow" "is" "big" "-")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2)) triple1) -> (rule2 % int1))
The cow is not big.
("cow" "is" "big" "-")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "young" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
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 chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow is rough.[(triple1)] @1: The cow is green.[(((triple1) -> rule3))] @2: The cow is blue.[(((((triple1) -> rule3)) -> rule1) OR ((((triple1) -> rule3)) -> rule4))] @3: The cow is not big.[(((((((triple1) -> rule3)) -> rule1) triple1) -> rule2) OR ((((((triple1) -> rule3)) -> rule4) triple1) -> rule2))]
The cow is rough.
("cow" "is" "rough" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
((triple1) -> (rule3 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not big.
("cow" "is" "big" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The cow is not big.
("cow" "is" "big" "-")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2)) triple1) -> (rule2 % int1))
The cow is not big.
("cow" "is" "big" "-")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3