Harry is kind. Harry is nice. Harry is young. All white, round things are nice. All young things are kind. If something is smart then it is kind. If something is nice then it is white. If something is round then it is nice. Kind, nice things are white. If Harry is nice and Harry is cold then Harry is white. Kind, white things are cold.
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is young.
("Harry" "is" "young" "+")
All white, round things are nice.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
All young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something is smart then it is kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
If something is nice then it is white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If something is round then it is nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Kind, nice things are white.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If Harry is nice and Harry is cold then Harry is white.
((("Harry" "is" "nice" "+") ("Harry" "is" "cold" "+")) -> ("Harry" "is" "white" "+"))
Kind, white things are cold.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Harry is nice.
True
1
proof
[(triple2)]
("Harry" "is" "nice" "+")
triple2
Harry is not kind.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule2))]
("Harry" "is" "kind" "-")
triple1
((triple3) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
True
2
proof
[(((triple2) -> rule4) OR ((triple1 triple2) -> rule6) OR ((((triple3) -> rule2) triple2) -> rule6))]
("Harry" "is" "white" "+")
((triple2) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple1 triple2) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple3) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not white.
False
2
inv-proof
[(((triple2) -> rule4) OR ((triple1 triple2) -> rule6) OR ((((triple3) -> rule2) triple2) -> rule6))]
("Harry" "is" "white" "-")
((triple2) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple1 triple2) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple3) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Harry is kind.[(triple1 OR ((triple3) -> rule2))] Harry is nice.[(triple2)] Harry is young.[(triple3)] @1: Harry is white.[(((triple2) -> rule4) OR ((triple1 triple2) -> rule6) OR ((((triple3) -> rule2) triple2) -> rule6))] @2: Harry is cold.[(((triple1 ((triple2) -> rule4)) -> rule8) OR ((triple1 ((triple1 triple2) -> rule6)) -> rule8) OR ((((triple3) -> rule2) ((triple2) -> rule4)) -> rule8) OR ((((triple3) -> rule2) ((triple1 triple2) -> rule6)) -> rule8) OR ((triple1 ((((triple3) -> rule2) triple2) -> rule6)) -> rule8) OR ((((triple3) -> rule2) ((((triple3) -> rule2) triple2) -> rule6)) -> rule8))]
Harry is kind.
("Harry" "is" "kind" "+")
triple1
((triple3) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
((triple2) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple1 triple2) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple3) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((triple1 ((triple2) -> (rule4 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((triple1 ((triple1 triple2) -> (rule6 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple3) -> (rule2 % int3)) ((triple2) -> (rule4 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((triple3) -> (rule2 % int3)) ((triple1 triple2) -> (rule6 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((triple1 ((((triple3) -> (rule2 % int3)) triple2) -> (rule6 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3)) triple2) -> (rule6 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3