The cow is blue. The cow is green. The cow is kind. The cow is nice. The cow is rough. Nice, rough people are blue. Rough people are blue. Green, nice people are blue. All rough people are blue. If someone is nice then they are blue. Nice people are green. All rough people are green. All blue people are nice.
The cow is blue.
("cow" "is" "blue" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is rough.
("cow" "is" "rough" "+")
Nice, rough people are blue.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
Rough people are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
Green, nice people are blue.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
All rough people are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If someone is nice then they are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
All rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
All blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
The cow is blue.
True
1
proof
[(triple1 OR ((triple4) -> rule5) OR ((triple5) -> rule2) OR ((triple5) -> rule4) OR ((triple2 triple4) -> rule3) OR ((triple4 triple5) -> rule1) OR ((((triple4) -> rule6) triple4) -> rule3) OR ((((triple5) -> rule7) triple4) -> rule3))]
("cow" "is" "blue" "+")
triple1
((triple4) -> (rule5 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple5) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple5) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple2 triple4) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple4 triple5) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((((triple4) -> (rule6 % int2)) triple4) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((triple5) -> (rule7 % int2)) triple4) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not nice.
False
1
inv-proof
[(triple4 OR ((triple1) -> rule8) OR ((((triple5) -> rule2)) -> rule8) OR ((((triple5) -> rule4)) -> rule8))]
("cow" "is" "nice" "-")
triple4
((triple1) -> (rule8 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule8 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
((((triple5) -> (rule4 % int2))) -> (rule8 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
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 chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow is blue.[(triple1 OR ((triple4) -> rule5) OR ((triple5) -> rule2) OR ((triple5) -> rule4) OR ((triple2 triple4) -> rule3) OR ((triple4 triple5) -> rule1) OR ((((triple4) -> rule6) triple4) -> rule3) OR ((((triple5) -> rule7) triple4) -> rule3))] The cow is green.[(triple2 OR ((triple4) -> rule6) OR ((triple5) -> rule7) OR ((((triple1) -> rule8)) -> rule6) OR ((((((triple5) -> rule2)) -> rule8)) -> rule6) OR ((((((triple5) -> rule4)) -> rule8)) -> rule6))] The cow is kind.[(triple3)] The cow is nice.[(triple4 OR ((triple1) -> rule8) OR ((((triple5) -> rule2)) -> rule8) OR ((((triple5) -> rule4)) -> rule8))] The cow is rough.[(triple5)]
The cow is blue.
("cow" "is" "blue" "+")
triple1
((triple4) -> (rule5 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple5) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple5) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple2 triple4) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple4 triple5) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((((triple4) -> (rule6 % int2)) triple4) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((triple5) -> (rule7 % int2)) triple4) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is green.
("cow" "is" "green" "+")
triple2
((triple4) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
((triple5) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
((((((triple5) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
((((((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
((triple1) -> (rule8 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule8 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
((((triple5) -> (rule4 % int2))) -> (rule8 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
triple5