Harry is red. All young things are smart. If Harry is smart then Harry is nice. Red things are young. If Harry is round and Harry is red then Harry is kind. If Harry is red then Harry is kind. If something is nice then it is kind.
Harry is red.
("Harry" "is" "red" "+")
All young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If Harry is smart then Harry is nice.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "nice" "+"))
Red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If Harry is round and Harry is red then Harry is kind.
((("Harry" "is" "round" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "kind" "+"))
If Harry is red then Harry is kind.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "kind" "+"))
If something is nice then it is kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Harry is red.
True
1
proof
[(triple1)]
("Harry" "is" "red" "+")
triple1
Harry is not red.
False
1
inv-proof
[(triple1)]
("Harry" "is" "red" "-")
triple1
Harry is young.
True
2
proof
[(((triple1) -> rule3))]
("Harry" "is" "young" "+")
((triple1) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple1) -> rule3))]
("Harry" "is" "young" "-")
((triple1) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Harry" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not smart.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Harry" "is" "smart" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is nice.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
("Harry" "is" "nice" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not nice.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
("Harry" "is" "nice" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Harry is red.[(triple1)] @1: Harry is kind.[(((triple1) -> rule5) OR ((((((((triple1) -> rule3)) -> rule1)) -> rule2)) -> rule6))] Harry is young.[(((triple1) -> rule3))] @2: Harry is smart.[(((((triple1) -> rule3)) -> rule1))] @3: Harry is nice.[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
Harry is red.
("Harry" "is" "red" "+")
triple1
Harry is kind.
("Harry" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((((((triple1) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
((triple1) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3