The cow is big. The cow is not blue. The cow is cold. The cow is round. The cow is not young. All round, blue people are young. All cold people are not young. If someone is young and not round then they are not cold. Big people are cold. If the cow is big then the cow is cold. If the cow is blue then the cow is 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 round.
("cow" "is" "round" "+")
The cow is not young.
("cow" "is" "young" "-")
All round, blue people are young.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
All cold people are not young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "-"))
If someone is young and not round then they are not cold.
((("someone" "is" "young" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "cold" "-"))
Big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If the cow is big then the cow is cold.
((("cow" "is" "big" "+")) -> ("cow" "is" "cold" "+"))
If the cow is blue then the cow is big.
((("cow" "is" "blue" "+")) -> ("cow" "is" "big" "+"))
The cow is not blue.
True
1
proof
[(triple2)]
("cow" "is" "blue" "-")
triple2
The cow is blue.
False
1
inv-proof
[(triple2)]
("cow" "is" "blue" "+")
triple2
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 visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cow is big.[(triple1)] The cow is cold.[(triple3 OR ((triple1) -> rule4) OR ((triple1) -> rule5))] The cow is not blue.[(triple2)] The cow is not young.[(triple5 OR ((triple3) -> rule2) OR ((((triple1) -> rule4)) -> rule2) OR ((((triple1) -> rule5)) -> rule2))] The cow is round.[(triple4)]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple3
((triple1) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple1) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is not blue.
("cow" "is" "blue" "-")
triple2
The cow is not young.
("cow" "is" "young" "-")
triple5
((triple3) -> (rule2 % int1))
The cow is not young.
("cow" "is" "young" "-")
int1
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The cow is not young.
("cow" "is" "young" "-")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The cow is not young.
("cow" "is" "young" "-")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is round.
("cow" "is" "round" "+")
triple4