The cow is blue. The cow is kind. The cow is red. The cow is rough. The cow is young. Young, kind people are blue. All blue people are kind. If the cow is kind and the cow is young then the cow is rough. If the cow is blue then the cow is rough. If someone is kind then they are young. If someone is blue and not kind then they are not red.
The cow is blue.
("cow" "is" "blue" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is young.
("cow" "is" "young" "+")
Young, kind people are blue.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If the cow is kind and the cow is young then the cow is rough.
((("cow" "is" "kind" "+") ("cow" "is" "young" "+")) -> ("cow" "is" "rough" "+"))
If the cow is blue then the cow is rough.
((("cow" "is" "blue" "+")) -> ("cow" "is" "rough" "+"))
If someone is kind then they are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If someone is blue and not kind then they are not red.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "red" "-"))
The cow is blue.
True
1
proof
[(triple1 OR ((triple5 triple2) -> rule1) OR ((((triple2) -> rule5) triple2) -> rule1))]
("cow" "is" "blue" "+")
triple1
((triple5 triple2) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((((triple2) -> (rule5 % int2)) triple2) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is not blue.
False
1
inv-proof
[(triple1 OR ((triple5 triple2) -> rule1) OR ((((triple2) -> rule5) triple2) -> rule1))]
("cow" "is" "blue" "-")
triple1
((triple5 triple2) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((((triple2) -> (rule5 % int2)) triple2) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow is blue.[(triple1 OR ((triple5 triple2) -> rule1) OR ((((triple2) -> rule5) triple2) -> rule1))] The cow is kind.[(triple2 OR ((triple1) -> rule2))] The cow is red.[(triple3)] The cow is rough.[(triple4 OR ((triple1) -> rule4) OR ((triple2 triple5) -> rule3) OR ((((triple5 triple2) -> rule1)) -> rule4) OR ((triple2 ((triple2) -> rule5)) -> rule3) OR ((((triple1) -> rule2) triple5) -> rule3) OR ((((triple1) -> rule2) ((triple2) -> rule5)) -> rule3) OR ((((((triple2) -> rule5) triple2) -> rule1)) -> rule4) OR ((triple2 ((((triple1) -> rule2)) -> rule5)) -> rule3) OR ((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule5)) -> rule3))] The cow is young.[(triple5 OR ((triple2) -> rule5) OR ((((triple1) -> rule2)) -> rule5))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
((triple5 triple2) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((((triple2) -> (rule5 % int2)) triple2) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
triple2
((triple1) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
triple3
The cow is rough.
("cow" "is" "rough" "+")
triple4
((triple1) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
((triple2 triple5) -> (rule3 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
((((triple5 triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
((((triple1) -> (rule2 % int2)) triple5) -> (rule3 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
((((triple1) -> (rule2 % int3)) ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
((((((triple2) -> (rule5 % int3)) triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is young.
("cow" "is" "young" "+")
int3
((triple2 ((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The cow is young.
("cow" "is" "young" "+")
triple5
((triple2) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2