The cow is cold. The cow is nice. The cow is round. If the cow is young then the cow is cold. Round people are nice. If the cow is blue and the cow is round then the cow is cold. Young people are blue. If someone is cold then they are young. If someone is cold then they are young. All nice, round people are cold. All blue, nice people are cold.
The cow is cold.
("cow" "is" "cold" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is round.
("cow" "is" "round" "+")
If the cow is young then the cow is cold.
((("cow" "is" "young" "+")) -> ("cow" "is" "cold" "+"))
Round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If the cow is blue and the cow is round then the cow is cold.
((("cow" "is" "blue" "+") ("cow" "is" "round" "+")) -> ("cow" "is" "cold" "+"))
Young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold then they are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If someone is cold then they are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All nice, round people are cold.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
All blue, nice people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
The cow is cold.
True
1
proof
[(triple1 OR ((triple2 triple3) -> rule7) OR ((((triple3) -> rule2) triple3) -> rule7))]
("cow" "is" "cold" "+")
triple1
((triple2 triple3) -> (rule7 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((((triple3) -> (rule2 % int2)) triple3) -> (rule7 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is not nice.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule2))]
("cow" "is" "nice" "-")
triple2
((triple3) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is young.
True
2
proof
[(((triple1) -> rule5) OR ((triple1) -> rule6) OR ((((triple2 triple3) -> rule7)) -> rule5) OR ((((triple2 triple3) -> rule7)) -> rule6) OR ((((((triple3) -> rule2) triple3) -> rule7)) -> rule5) OR ((((((triple3) -> rule2) triple3) -> rule7)) -> rule6))]
("cow" "is" "young" "+")
((triple1) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((triple1) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((((triple2 triple3) -> (rule7 % int2))) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple2 triple3) -> (rule7 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((((triple3) -> (rule2 % int3)) triple3) -> (rule7 % int2))) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
((((((triple3) -> (rule2 % int3)) triple3) -> (rule7 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The cow is not young.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple1) -> rule6) OR ((((triple2 triple3) -> rule7)) -> rule5) OR ((((triple2 triple3) -> rule7)) -> rule6) OR ((((((triple3) -> rule2) triple3) -> rule7)) -> rule5) OR ((((((triple3) -> rule2) triple3) -> rule7)) -> rule6))]
("cow" "is" "young" "-")
((triple1) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((triple1) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((((triple2 triple3) -> (rule7 % int2))) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple2 triple3) -> (rule7 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((((triple3) -> (rule2 % int3)) triple3) -> (rule7 % int2))) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
((((((triple3) -> (rule2 % int3)) triple3) -> (rule7 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The cow is blue.
True
3
proof
[(((((triple1) -> rule5)) -> rule4) OR ((((triple1) -> rule6)) -> rule4) OR ((((((triple2 triple3) -> rule7)) -> rule5)) -> rule4) OR ((((((triple2 triple3) -> rule7)) -> rule6)) -> rule4) OR ((((((((triple3) -> rule2) triple3) -> rule7)) -> rule5)) -> rule4) OR ((((((((triple3) -> rule2) triple3) -> rule7)) -> rule6)) -> rule4))]
("cow" "is" "blue" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
((((((triple2 triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((((triple2 triple3) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((((((triple3) -> (rule2 % int4)) triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is nice.
("cow" "is" "nice" "+")
int4
((((((((triple3) -> (rule2 % int4)) triple3) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is nice.
("cow" "is" "nice" "+")
int4
The cow is not blue.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4) OR ((((triple1) -> rule6)) -> rule4) OR ((((((triple2 triple3) -> rule7)) -> rule5)) -> rule4) OR ((((((triple2 triple3) -> rule7)) -> rule6)) -> rule4) OR ((((((((triple3) -> rule2) triple3) -> rule7)) -> rule5)) -> rule4) OR ((((((((triple3) -> rule2) triple3) -> rule7)) -> rule6)) -> rule4))]
("cow" "is" "blue" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
((((((triple2 triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((((triple2 triple3) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((((((triple3) -> (rule2 % int4)) triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is nice.
("cow" "is" "nice" "+")
int4
((((((((triple3) -> (rule2 % int4)) triple3) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is nice.
("cow" "is" "nice" "+")
int4
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 cold.[(triple1 OR ((triple2 triple3) -> rule7) OR ((((triple3) -> rule2) triple3) -> rule7))] The cow is nice.[(triple2 OR ((triple3) -> rule2))] The cow is round.[(triple3)] @1: The cow is young.[(((triple1) -> rule5) OR ((triple1) -> rule6) OR ((((triple2 triple3) -> rule7)) -> rule5) OR ((((triple2 triple3) -> rule7)) -> rule6) OR ((((((triple3) -> rule2) triple3) -> rule7)) -> rule5) OR ((((((triple3) -> rule2) triple3) -> rule7)) -> rule6))] @2: The cow is blue.[(((((triple1) -> rule5)) -> rule4) OR ((((triple1) -> rule6)) -> rule4) OR ((((((triple2 triple3) -> rule7)) -> rule5)) -> rule4) OR ((((((triple2 triple3) -> rule7)) -> rule6)) -> rule4) OR ((((((((triple3) -> rule2) triple3) -> rule7)) -> rule5)) -> rule4) OR ((((((((triple3) -> rule2) triple3) -> rule7)) -> rule6)) -> rule4))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
((triple2 triple3) -> (rule7 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((((triple3) -> (rule2 % int2)) triple3) -> (rule7 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
triple2
((triple3) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is round.
("cow" "is" "round" "+")
triple3
The cow is young.
("cow" "is" "young" "+")
((triple1) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((triple1) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((((triple2 triple3) -> (rule7 % int2))) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple2 triple3) -> (rule7 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((((triple3) -> (rule2 % int3)) triple3) -> (rule7 % int2))) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
((((((triple3) -> (rule2 % int3)) triple3) -> (rule7 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
((((((triple2 triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((((triple2 triple3) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((((((triple3) -> (rule2 % int4)) triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is nice.
("cow" "is" "nice" "+")
int4
((((((((triple3) -> (rule2 % int4)) triple3) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is nice.
("cow" "is" "nice" "+")
int4