Dave is furry. Dave is nice. Dave is round. Gary is blue. Gary is furry. Gary is red. Harry is kind. Harry is nice. Harry is round. Harry is white. All kind things are blue. All nice things are white. If something is round then it is red.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
All nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Harry is white.
True
1
proof
[(triple10 OR ((triple8) -> rule2))]
("Harry" "is" "white" "+")
triple10
((triple8) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Gary is not red.
False
1
inv-proof
[(triple6)]
("Gary" "is" "red" "-")
triple6
Harry is red.
True
2
proof
[(((triple9) -> rule3))]
("Harry" "is" "red" "+")
((triple9) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "white" "-")
((triple2) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "blue" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "white" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Dave is furry.[(triple1)] Dave is nice.[(triple2)] Dave is round.[(triple3)] Gary is blue.[(triple4)] Gary is furry.[(triple5)] Gary is red.[(triple6)] Harry is kind.[(triple7)] Harry is nice.[(triple8)] Harry is round.[(triple9)] Harry is white.[(triple10 OR ((triple8) -> rule2))] @1: Dave is red.[(((triple3) -> rule3))] Dave is white.[(((triple2) -> rule2))] Harry is blue.[(((triple7) -> rule1))] Harry is red.[(((triple9) -> rule3))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
((triple8) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple3) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple2) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple9) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1