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