Gary is red. Harry is rough. Harry is smart. Red, nice things are blue. If Harry is nice then Harry is red. If something is smart then it is quiet. All smart, quiet things are red. If Harry is furry and Harry is blue then Harry is nice. If something is furry then it is red.
Gary is red.
("Gary" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Red, nice things are blue.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If Harry is nice then Harry is red.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "red" "+"))
If something is smart then it is quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
All smart, quiet things are red.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If Harry is furry and Harry is blue then Harry is nice.
((("Harry" "is" "furry" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "nice" "+"))
If something is furry then it is red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Harry is smart.
True
1
proof
[(triple3)]
("Harry" "is" "smart" "+")
triple3
Gary is not red.
False
1
inv-proof
[(triple1)]
("Gary" "is" "red" "-")
triple1
Harry is quiet.
True
2
proof
[(((triple3) -> rule3))]
("Harry" "is" "quiet" "+")
((triple3) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "quiet" "-")
((triple3) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
True
4
proof
[(((triple3 ((triple3) -> rule3)) -> rule4))]
("Harry" "is" "red" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not red.
False
4
inv-proof
[(((triple3 ((triple3) -> rule3)) -> rule4))]
("Harry" "is" "red" "-")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not blue.
Unknown
inv-rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Harry" "is" "blue" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "blue" "+")
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Gary is red.[(triple1)] Harry is rough.[(triple2)] Harry is smart.[(triple3)] @1: Harry is quiet.[(((triple3) -> rule3))] @2: Harry is red.[(((triple3 ((triple3) -> rule3)) -> rule4))]
Gary is red.
("Gary" "is" "red" "+")
triple1
Harry is rough.
("Harry" "is" "rough" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple3) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2