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