Bob is big. Bob is red. Bob is round. Bob is smart. Bob is young. Dave is big. Dave is blue. Dave is nice. Dave is not red. Dave is round. Dave is smart. Dave is young. Harry is nice. Harry is red. Harry is round. Harry is young. If something is red then it is big. If Dave is blue then Dave is round. If Bob is not blue then Bob is not young. If Harry is round then Harry is red. If something is round and not red then it is smart. If something is red and smart then it is not nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is red then it is big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If Dave is blue then Dave is round.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "round" "+"))
If Bob is not blue then Bob is not young.
((("Bob" "is" "blue" "~")) -> ("Bob" "is" "young" "-"))
If Harry is round then Harry is red.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "red" "+"))
If something is round and not red then it is smart.
((("something" "is" "round" "+") ("something" "is" "red" "~")) -> ("something" "is" "smart" "+"))
If something is red and smart then it is not nice.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "-"))
Bob is big.
True
1
proof
[(triple1 OR ((triple2) -> rule1))]
("Bob" "is" "big" "+")
triple1
((triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not young.
False
1
inv-proof
[(triple5)]
("Bob" "is" "young" "-")
triple5
Harry is big.
True
2
proof
[(((triple14) -> rule1) OR ((((triple15) -> rule4)) -> rule1))]
("Harry" "is" "big" "+")
((triple14) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple15) -> (rule4 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Bob is nice.
False
3
inv-proof
[(((triple2 triple4) -> rule6))]
("Bob" "is" "nice" "+")
((triple2 triple4) -> (rule6 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "smart" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is big.[(triple1 OR ((triple2) -> rule1))] Bob is red.[(triple2)] Bob is round.[(triple3)] Bob is smart.[(triple4)] Bob is young.[(triple5)] Dave is big.[(triple6)] Dave is blue.[(triple7)] Dave is nice.[(triple8)] Dave is not red.[(triple9)] Dave is round.[(triple10 OR ((triple7) -> rule2))] Dave is smart.[(triple11 OR ((triple10 triple9) -> rule5) OR ((((triple7) -> rule2) triple9) -> rule5))] Dave is young.[(triple12)] Harry is nice.[(triple13)] Harry is red.[(triple14 OR ((triple15) -> rule4))] Harry is round.[(triple15)] Harry is young.[(triple16)] @1: Bob is not nice.[(((triple2 triple4) -> rule6))] Harry is big.[(((triple14) -> rule1) OR ((((triple15) -> rule4)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is blue.
("Dave" "is" "blue" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
triple8
Dave is not red.
("Dave" "is" "red" "-")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
((triple7) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple11
((triple10 triple9) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple7) -> (rule2 % int2)) triple9) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
triple13
Harry is red.
("Harry" "is" "red" "+")
triple14
((triple15) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
Bob is not nice.
("Bob" "is" "nice" "-")
((triple2 triple4) -> (rule6 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple14) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple15) -> (rule4 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2