Bob is green. Bob is white. Harry is blue. Harry is furry. Harry is green. Harry is kind. Harry is round. All cold, kind things are green. White, kind things are green. If Harry is blue then Harry is round. If something is blue and round then it is cold. If Harry is green and Harry is white then Harry is furry. If Harry is blue and Harry is round then Harry is furry.
Bob is green.
("Bob" "is" "green" "+")
Bob is white.
("Bob" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
All cold, kind things are green.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
White, kind things are green.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If Harry is blue then Harry is round.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "round" "+"))
If something is blue and round then it is cold.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If Harry is green and Harry is white then Harry is furry.
((("Harry" "is" "green" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "furry" "+"))
If Harry is blue and Harry is round then Harry is furry.
((("Harry" "is" "blue" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "furry" "+"))
Harry is green.
True
1
proof
[(triple5 OR ((((triple3 triple7) -> rule4) triple6) -> rule1) OR ((((triple3 ((triple3) -> rule3)) -> rule4) triple6) -> rule1))]
("Harry" "is" "green" "+")
triple5
((((triple3 triple7) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Bob is not green.
False
1
inv-proof
[(triple1)]
("Bob" "is" "green" "-")
triple1
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is green.[(triple1)] Bob is white.[(triple2)] Harry is blue.[(triple3)] Harry is furry.[(triple4 OR ((triple3 triple7) -> rule6) OR ((triple3 ((triple3) -> rule3)) -> rule6))] Harry is green.[(triple5 OR ((((triple3 triple7) -> rule4) triple6) -> rule1) OR ((((triple3 ((triple3) -> rule3)) -> rule4) triple6) -> rule1))] Harry is kind.[(triple6)] Harry is round.[(triple7 OR ((triple3) -> rule3))] @1: Harry is cold.[(((triple3 triple7) -> rule4) OR ((triple3 ((triple3) -> rule3)) -> rule4))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
((triple3 triple7) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple3 ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple5
((((triple3 triple7) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
((triple3) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple3 triple7) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2