Bob is not green. Bob is not nice. Bob is white. Dave is kind. Dave is nice. Dave is not young. Harry is green. Harry is not kind. Harry is not white. Harry is not young. Green, young people are not blue. Round people are not young. If someone is nice and not green then they are young. If someone is blue then they are not round. If Harry is young then Harry is blue. If someone is green then they are not nice.
Bob is not green.
("Bob" "is" "green" "-")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is white.
("Bob" "is" "white" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not young.
("Dave" "is" "young" "-")
Harry is green.
("Harry" "is" "green" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is not white.
("Harry" "is" "white" "-")
Harry is not young.
("Harry" "is" "young" "-")
Green, young people are not blue.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "-"))
Round people are not young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "-"))
If someone is nice and not green then they are young.
((("someone" "is" "nice" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "young" "+"))
If someone is blue then they are not round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "-"))
If Harry is young then Harry is blue.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "blue" "+"))
If someone is green then they are not nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "-"))
Harry is green.
True
1
proof
[(triple7)]
("Harry" "is" "green" "+")
triple7
Bob is nice.
False
1
inv-proof
[(triple2)]
("Bob" "is" "nice" "+")
triple2
Harry is not nice.
True
2
proof
[(((triple7) -> rule6))]
("Harry" "is" "nice" "-")
((triple7) -> (rule6 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is nice.
False
2
inv-proof
[(((triple7) -> rule6))]
("Harry" "is" "nice" "+")
((triple7) -> (rule6 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "young" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "blue" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Bob is not green.[(triple1)] Bob is not nice.[(triple2)] Bob is white.[(triple3)] Dave is kind.[(triple4)] Dave is nice.[(triple5)] Dave is not young.[(triple6)] Harry is green.[(triple7)] Harry is not kind.[(triple8)] Harry is not white.[(triple9)] Harry is not young.[(triple10)] @1: Harry is not nice.[(((triple7) -> rule6))]
Bob is not green.
("Bob" "is" "green" "-")
triple1
Bob is not nice.
("Bob" "is" "nice" "-")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is not young.
("Dave" "is" "young" "-")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Harry is not kind.
("Harry" "is" "kind" "-")
triple8
Harry is not white.
("Harry" "is" "white" "-")
triple9
Harry is not young.
("Harry" "is" "young" "-")
triple10
Harry is not nice.
("Harry" "is" "nice" "-")
((triple7) -> (rule6 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1