The cow is blue. The cow is cold. The cow is green. The cow is nice. The cow is round. All green people are round. Blue people are round. Cold people are nice. All round people are nice. If someone is cold then they are nice. Round, green people are blue. All blue people are green. If the cow is blue and the cow is not cold then the cow is nice.
The cow is blue.
("cow" "is" "blue" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is round.
("cow" "is" "round" "+")
All green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
Cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
All round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold then they are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
Round, green people are blue.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
All blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If the cow is blue and the cow is not cold then the cow is nice.
((("cow" "is" "blue" "+") ("cow" "is" "cold" "~")) -> ("cow" "is" "nice" "+"))
The cow is blue.
True
1
proof
[(triple1 OR ((triple5 triple3) -> rule6) OR ((((triple3) -> rule1) triple3) -> rule6))]
("cow" "is" "blue" "+")
triple1
((triple5 triple3) -> (rule6 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((((triple3) -> (rule1 % int2)) triple3) -> (rule6 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow is not nice.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule3) OR ((triple2) -> rule5) OR ((triple5) -> rule4) OR ((((triple1) -> rule2)) -> rule4) OR ((((triple3) -> rule1)) -> rule4) OR ((((((triple1) -> rule7)) -> rule1)) -> rule4))]
("cow" "is" "nice" "-")
triple4
((triple2) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
((triple2) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
((triple5) -> (rule4 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
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 blue.[(triple1 OR ((triple5 triple3) -> rule6) OR ((((triple3) -> rule1) triple3) -> rule6))] The cow is cold.[(triple2)] The cow is green.[(triple3 OR ((triple1) -> rule7))] The cow is nice.[(triple4 OR ((triple2) -> rule3) OR ((triple2) -> rule5) OR ((triple5) -> rule4) OR ((((triple1) -> rule2)) -> rule4) OR ((((triple3) -> rule1)) -> rule4) OR ((((((triple1) -> rule7)) -> rule1)) -> rule4))] The cow is round.[(triple5 OR ((triple1) -> rule2) OR ((triple3) -> rule1) OR ((((triple1) -> rule7)) -> rule1))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
((triple5 triple3) -> (rule6 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((((triple3) -> (rule1 % int2)) triple3) -> (rule6 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
((triple1) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
triple4
((triple2) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
((triple2) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
((triple5) -> (rule4 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow is round.
("cow" "is" "round" "+")
triple5
((triple1) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
((triple3) -> (rule1 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2