Bob is furry. Bob is green. Bob is kind. Charlie is blue. Charlie is cold. Charlie is furry. Charlie is green. Charlie is kind. Charlie is quiet. Harry is cold. Harry is furry. Harry is quiet. All green things are cold. If something is green then it is cold.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Bob is green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "+")
triple2
Charlie is not blue.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "blue" "-")
triple4
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Bob is furry.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3)] Charlie is blue.[(triple4)] Charlie is cold.[(triple5 OR ((triple7) -> rule1) OR ((triple7) -> rule2))] Charlie is furry.[(triple6)] Charlie is green.[(triple7)] Charlie is kind.[(triple8)] Charlie is quiet.[(triple9)] Harry is cold.[(triple10)] Harry is furry.[(triple11)] Harry is quiet.[(triple12)] @1: Bob is cold.[(((triple2) -> rule1) OR ((triple2) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
((triple7) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple7) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
triple8
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple2) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1