The cow is cold. The cow is kind. The cow is red. If the cow is red and the cow is green then the cow is cold. Green people are kind. All kind, blue people are red. If the cow is cold and the cow is green then the cow is red. Kind people are cold. All blue, kind people are red. If the cow is kind then the cow is green. All blue people are cold.
The cow is cold.
("cow" "is" "cold" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is red.
("cow" "is" "red" "+")
If the cow is red and the cow is green then the cow is cold.
((("cow" "is" "red" "+") ("cow" "is" "green" "+")) -> ("cow" "is" "cold" "+"))
Green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
All kind, blue people are red.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If the cow is cold and the cow is green then the cow is red.
((("cow" "is" "cold" "+") ("cow" "is" "green" "+")) -> ("cow" "is" "red" "+"))
Kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
All blue, kind people are red.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If the cow is kind then the cow is green.
((("cow" "is" "kind" "+")) -> ("cow" "is" "green" "+"))
All blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
The cow is cold.
True
1
proof
[(triple1 OR ((triple2) -> rule5) OR ((triple3 ((triple2) -> rule7)) -> rule1))]
("cow" "is" "cold" "+")
triple1
((triple2) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple3 ((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not cold.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule5) OR ((triple3 ((triple2) -> rule7)) -> rule1))]
("cow" "is" "cold" "-")
triple1
((triple2) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple3 ((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is green.
("cow" "is" "green" "+")
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 is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
@0: The cow is cold.[(triple1 OR ((triple2) -> rule5) OR ((triple3 ((triple2) -> rule7)) -> rule1))] The cow is kind.[(triple2)] The cow is red.[(triple3 OR ((triple1 ((triple2) -> rule7)) -> rule4) OR ((((triple2) -> rule5) ((triple2) -> rule7)) -> rule4))] @1: The cow is green.[(((triple2) -> rule7))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
((triple2) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple3 ((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
triple2
The cow is red.
("cow" "is" "red" "+")
triple3
((triple1 ((triple2) -> (rule7 % int2))) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((triple2) -> (rule5 % int3)) ((triple2) -> (rule7 % int2))) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is green.
("cow" "is" "green" "+")
((triple2) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1