Bob is big. Bob is green. Bob is round. Harry is big. Harry is nice. Harry is red. Harry is smart. If Bob is green then Bob is round. If Bob is red then Bob is green. If something is white and red then it is round. If Harry is big then Harry is nice. Red things are round. White things are nice. If something is big and red then it is white. All white things are red.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Bob is green then Bob is round.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "round" "+"))
If Bob is red then Bob is green.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "green" "+"))
If something is white and red then it is round.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
If Harry is big then Harry is nice.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "nice" "+"))
Red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
White things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is big and red then it is white.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
All white things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
Bob is round.
True
1
proof
[(triple3 OR ((triple2) -> rule1))]
("Bob" "is" "round" "+")
triple3
((triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Bob is not white.
Unknown
inv-rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is big.[(triple1)] Bob is green.[(triple2)] Bob is round.[(triple3 OR ((triple2) -> rule1))] Harry is big.[(triple4)] Harry is nice.[(triple5 OR ((triple4) -> rule4) OR ((((triple4 triple6) -> rule7)) -> rule6))] Harry is red.[(triple6)] Harry is smart.[(triple7)] @1: Harry is round.[(((triple6) -> rule5) OR ((((triple4 triple6) -> rule7) triple6) -> rule3))] Harry is white.[(((triple4 triple6) -> rule7))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
((triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple4
Harry is nice.
("Harry" "is" "nice" "+")
triple5
((triple4) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple4 triple6) -> (rule7 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Harry is round.
("Harry" "is" "round" "+")
((triple6) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple4 triple6) -> (rule7 % int2)) triple6) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((triple4 triple6) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1