Bob is not blue. Bob is cold. Bob is not green. Bob is kind. Bob is young. Dave is cold. Dave is red. Dave is young. Harry is not cold. Harry is not young. If something is quiet and not young then it is green. If something is red and not young then it is kind. All cold things are kind. If Bob is blue and Bob is quiet then Bob is kind. If Harry is green then Harry is quiet. Cold things are not quiet. All quiet things are blue. If Bob is quiet and Bob is young then Bob is blue.
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is not young.
("Harry" "is" "young" "-")
If something is quiet and not young then it is green.
((("something" "is" "quiet" "+") ("something" "is" "young" "~")) -> ("something" "is" "green" "+"))
If something is red and not young then it is kind.
((("something" "is" "red" "+") ("something" "is" "young" "~")) -> ("something" "is" "kind" "+"))
All cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If Bob is blue and Bob is quiet then Bob is kind.
((("Bob" "is" "blue" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "kind" "+"))
If Harry is green then Harry is quiet.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "quiet" "+"))
Cold things are not quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "-"))
All quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If Bob is quiet and Bob is young then Bob is blue.
((("Bob" "is" "quiet" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "blue" "+"))
Dave is red.
True
1
proof
[(triple7)]
("Dave" "is" "red" "+")
triple7
Harry is cold.
False
1
inv-proof
[(triple9)]
("Harry" "is" "cold" "+")
triple9
Harry is not blue.
Unknown
inv-rconc
[@3: Harry is blue.[CWA. Example of deepest failure = (rule7 <- rule5 <- rule1 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Bob is cold.[(triple2)] Bob is kind.[(triple4 OR ((triple2) -> rule3))] Bob is not blue.[(triple1)] Bob is not green.[(triple3)] Bob is young.[(triple5)] Dave is cold.[(triple6)] Dave is red.[(triple7)] Dave is young.[(triple8)] Harry is not cold.[(triple9)] Harry is not young.[(triple10)] @1: Bob is not quiet.[(((triple2) -> rule6))] Dave is kind.[(((triple6) -> rule3))] Dave is not quiet.[(((triple6) -> rule6))]
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
triple1
Bob is not green.
("Bob" "is" "green" "-")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple5
Dave is cold.
("Dave" "is" "cold" "+")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple8
Harry is not cold.
("Harry" "is" "cold" "-")
triple9
Harry is not young.
("Harry" "is" "young" "-")
triple10
Bob is not quiet.
("Bob" "is" "quiet" "-")
((triple2) -> (rule6 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple6) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not quiet.
("Dave" "is" "quiet" "-")
((triple6) -> (rule6 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1