Bob is blue. Bob is green. Bob is round. Bob is smart. Bob is white. Harry is blue. Harry is green. Harry is nice. Harry is rough. Harry is white. All rough, blue things are white. If Bob is smart then Bob is rough.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
All rough, blue things are white.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If Bob is smart then Bob is rough.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "rough" "+"))
Harry is rough.
True
1
proof
[(triple9)]
("Harry" "is" "rough" "+")
triple9
Harry is not white.
False
1
inv-proof
[(triple10 OR ((triple9 triple6) -> rule1))]
("Harry" "is" "white" "-")
triple10
((triple9 triple6) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Bob is blue.[(triple1)] Bob is green.[(triple2)] Bob is round.[(triple3)] Bob is smart.[(triple4)] Bob is white.[(triple5 OR ((((triple4) -> rule2) triple1) -> rule1))] Harry is blue.[(triple6)] Harry is green.[(triple7)] Harry is nice.[(triple8)] Harry is rough.[(triple9)] Harry is white.[(triple10 OR ((triple9 triple6) -> rule1))] @1: Bob is rough.[(((triple4) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
((((triple4) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
((triple9 triple6) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple4) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1