The cow is big. The cow is not blue. The cow is cold. The cow is green. The cow is rough. Green things are rough. If something is big then it is green. Rough things are big.
The cow is big.
("cow" "is" "big" "+")
The cow is not blue.
("cow" "is" "blue" "-")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is rough.
("cow" "is" "rough" "+")
Green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
If something is big then it is green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
The cow is rough.
True
1
proof
[(triple5 OR ((triple4) -> rule1) OR ((((triple1) -> rule2)) -> rule1))]
("cow" "is" "rough" "+")
triple5
((triple4) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not cold.
False
1
inv-proof
[(triple3)]
("cow" "is" "cold" "-")
triple3
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 chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow is big.[(triple1 OR ((triple5) -> rule3) OR ((((triple4) -> rule1)) -> rule3))] The cow is cold.[(triple3)] The cow is green.[(triple4 OR ((triple1) -> rule2) OR ((((triple5) -> rule3)) -> rule2))] The cow is not blue.[(triple2)] The cow is rough.[(triple5 OR ((triple4) -> rule1) OR ((((triple1) -> rule2)) -> rule1))]
The cow is big.
("cow" "is" "big" "+")
triple1
((triple5) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
triple3
The cow is green.
("cow" "is" "green" "+")
triple4
((triple1) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is not blue.
("cow" "is" "blue" "-")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple5
((triple4) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2