Bob is green. Bob is round. Dave is blue. Dave is cold. Dave is furry. Dave is not green. Dave is quiet. Dave is round. Gary is blue. Gary is furry. Gary is kind. Gary is not round. Harry is cold. Harry is furry. Harry is round. All quiet things are blue. If something is kind then it is green. Quiet, blue things are not green. If something is kind and furry then it is green. Green things are kind. If something is cold then it is quiet.
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not round.
("Gary" "is" "round" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is round.
("Harry" "is" "round" "+")
All quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is kind then it is green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Quiet, blue things are not green.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "-"))
If something is kind and furry then it is green.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
Green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is cold then it is quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Gary is blue.
True
1
proof
[(triple9)]
("Gary" "is" "blue" "+")
triple9
Dave is not round.
False
1
inv-proof
[(triple8)]
("Dave" "is" "round" "-")
triple8
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "kind" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Bob is green.[(triple1)] Bob is round.[(triple2)] Dave is blue.[(triple3 OR ((triple7) -> rule1) OR ((((triple4) -> rule6)) -> rule1))] Dave is cold.[(triple4)] Dave is furry.[(triple5)] Dave is not green.[(triple6 OR ((triple7 triple3) -> rule3) OR ((triple7 ((triple7) -> rule1)) -> rule3) OR ((((triple4) -> rule6) triple3) -> rule3) OR ((((triple4) -> rule6) ((triple7) -> rule1)) -> rule3) OR ((triple7 ((((triple4) -> rule6)) -> rule1)) -> rule3) OR ((((triple4) -> rule6) ((((triple4) -> rule6)) -> rule1)) -> rule3))] Dave is quiet.[(triple7 OR ((triple4) -> rule6))] Dave is round.[(triple8)] Gary is blue.[(triple9)] Gary is furry.[(triple10)] Gary is kind.[(triple11)] Gary is not round.[(triple12)] Harry is cold.[(triple13)] Harry is furry.[(triple14)] Harry is round.[(triple15)] @1: Bob is kind.[(((triple1) -> rule5))] Gary is green.[(((triple11) -> rule2) OR ((triple11 triple10) -> rule4))] Harry is quiet.[(((triple13) -> rule6))] @2: Harry is blue.[(((((triple13) -> rule6)) -> rule1))] @3: Harry is not green.[(((((triple13) -> rule6) ((((triple13) -> rule6)) -> rule1)) -> rule3))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
((triple7) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is not green.
("Dave" "is" "green" "-")
triple6
((triple7 triple3) -> (rule3 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
((triple7 ((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple4) -> (rule6 % int2)) triple3) -> (rule3 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple4) -> (rule6 % int3)) ((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((triple7 ((((triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((triple4) -> (rule6 % int3)) ((((triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
((triple4) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is furry.
("Gary" "is" "furry" "+")
triple10
Gary is kind.
("Gary" "is" "kind" "+")
triple11
Gary is not round.
("Gary" "is" "round" "-")
triple12
Harry is cold.
("Harry" "is" "cold" "+")
triple13
Harry is furry.
("Harry" "is" "furry" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple11) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple11 triple10) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple13) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple13) -> (rule6 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not green.
("Harry" "is" "green" "-")
((((triple13) -> (rule6 % int3)) ((((triple13) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3