Harry is blue. Harry is kind. Harry is red. Kind, green people are blue. If someone is young then they are kind. If someone is blue and green then they are rough. If someone is kind then they are rough. Blue people are red. If Harry is rough then Harry is green.
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Kind, green people are blue.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is young then they are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue and green then they are rough.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind then they are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
Blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If Harry is rough then Harry is green.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "green" "+"))
Harry is red.
True
1
proof
[(triple3 OR ((triple1) -> rule5) OR ((((triple2 ((((triple2) -> rule4)) -> rule6)) -> rule1)) -> rule5))]
("Harry" "is" "red" "+")
triple3
((triple1) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple2 ((((triple2) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is not kind.
False
1
inv-proof
[(triple2)]
("Harry" "is" "kind" "-")
triple2
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Harry is blue.[(triple1 OR ((triple2 ((((triple2) -> rule4)) -> rule6)) -> rule1))] Harry is kind.[(triple2)] Harry is red.[(triple3 OR ((triple1) -> rule5) OR ((((triple2 ((((triple2) -> rule4)) -> rule6)) -> rule1)) -> rule5))] @1: Harry is rough.[(((triple2) -> rule4))] @2: Harry is green.[(((((triple2) -> rule4)) -> rule6))]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
((triple1) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple2 ((((triple2) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
((triple2) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2