Bob is big. Bob is cold. Bob is kind. Bob is red. Bob is rough. Harry is blue. Harry is cold. Harry is kind. Harry is not red. Harry is round. If something is rough then it is round. If something is rough and not round then it is not blue.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is round.
("Harry" "is" "round" "+")
If something is rough then it is round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is rough and not round then it is not blue.
((("something" "is" "rough" "+") ("something" "is" "round" "~")) -> ("something" "is" "blue" "-"))
Bob is rough.
True
1
proof
[(triple5)]
("Bob" "is" "rough" "+")
triple5
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Bob is round.
True
2
proof
[(((triple5) -> rule1))]
("Bob" "is" "round" "+")
((triple5) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple5) -> rule1))]
("Bob" "is" "round" "-")
((triple5) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is kind.[(triple3)] Bob is red.[(triple4)] Bob is rough.[(triple5)] Harry is blue.[(triple6)] Harry is cold.[(triple7)] Harry is kind.[(triple8)] Harry is not red.[(triple9)] Harry is round.[(triple10)] @1: Bob is round.[(((triple5) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple8
Harry is not red.
("Harry" "is" "red" "-")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
Bob is round.
("Bob" "is" "round" "+")
((triple5) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1