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