Bob is green. Erin is green. Gary is round. Harry is green. All smart things are not blue. All red things are not blue. All round things are green. Nice, red things are green. If Harry is nice then Harry is red. If something is blue and round then it is not nice.
Bob is green.
("Bob" "is" "green" "+")
Erin is green.
("Erin" "is" "green" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is green.
("Harry" "is" "green" "+")
All smart things are not blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "-"))
All red things are not blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "-"))
All round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Nice, red things are green.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If Harry is nice then Harry is red.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "red" "+"))
If something is blue and round then it is not nice.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "-"))
Gary is round.
True
1
proof
[(triple3)]
("Gary" "is" "round" "+")
triple3
Harry is not green.
False
1
inv-proof
[(triple4)]
("Harry" "is" "green" "-")
triple4
Gary is green.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "green" "+")
((triple3) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "green" "-")
((triple3) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "red" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Bob is green.[(triple1)] Erin is green.[(triple2)] Gary is round.[(triple3)] Harry is green.[(triple4)] @1: Gary is green.[(((triple3) -> rule3))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
((triple3) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1