The cow is rough. The cow is not round. The cow is young. Round, young things are not cold. If something is round then it is cold. Red, rough things are cold. If something is cold and round then it is young. All rough things are red. All rough things are red. If something is round then it is rough. If the cow is not round then the cow is red.
The cow is rough.
("cow" "is" "rough" "+")
The cow is not round.
("cow" "is" "round" "-")
The cow is young.
("cow" "is" "young" "+")
Round, young things are not cold.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "-"))
If something is round then it is cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Red, rough things are cold.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is cold and round then it is young.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
All rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something is round then it is rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If the cow is not round then the cow is red.
((("cow" "is" "round" "~")) -> ("cow" "is" "red" "+"))
The cow is young.
True
1
proof
[(triple3)]
("cow" "is" "young" "+")
triple3
The cow is round.
False
1
inv-proof
[(triple2)]
("cow" "is" "round" "+")
triple2
The cow is red.
True
2
proof
[(((triple1) -> rule5) OR ((triple1) -> rule6) OR ((triple2) -> rule8))]
("cow" "is" "red" "+")
((triple1) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
((triple1) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
((triple2) -> (rule8 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is not red.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple1) -> rule6) OR ((triple2) -> rule8))]
("cow" "is" "red" "-")
((triple1) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
((triple1) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
((triple2) -> (rule8 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
True
4
proof
[(((((triple1) -> rule5) triple1) -> rule3) OR ((((triple1) -> rule6) triple1) -> rule3) OR ((((triple2) -> rule8) triple1) -> rule3))]
("cow" "is" "cold" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
((((triple1) -> (rule6 % int2)) triple1) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
((((triple2) -> (rule8 % int2)) triple1) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is not cold.
False
4
inv-proof
[(((((triple1) -> rule5) triple1) -> rule3) OR ((((triple1) -> rule6) triple1) -> rule3) OR ((((triple2) -> rule8) triple1) -> rule3))]
("cow" "is" "cold" "-")
((((triple1) -> (rule5 % int2)) triple1) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
((((triple1) -> (rule6 % int2)) triple1) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
((((triple2) -> (rule8 % int2)) triple1) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow is not round.[(triple2)] The cow is rough.[(triple1)] The cow is young.[(triple3)] @1: The cow is red.[(((triple1) -> rule5) OR ((triple1) -> rule6) OR ((triple2) -> rule8))] @2: The cow is cold.[(((((triple1) -> rule5) triple1) -> rule3) OR ((((triple1) -> rule6) triple1) -> rule3) OR ((((triple2) -> rule8) triple1) -> rule3))]
The cow is not round.
("cow" "is" "round" "-")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple1
The cow is young.
("cow" "is" "young" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
((triple1) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
((triple1) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
((triple2) -> (rule8 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
((((triple1) -> (rule6 % int2)) triple1) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
((((triple2) -> (rule8 % int2)) triple1) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2