Bob is blue. Bob is green. Bob is kind. Bob is quiet. Bob is round. Bob is smart. Charlie is green. Charlie is round. Charlie is smart. Gary is blue. Gary is green. Gary is round. Harry is kind. Harry is quiet. Harry is red. If something is round and quiet then it is smart. If Harry is quiet then Harry is round. All smart, red things are quiet.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
If something is round and quiet then it is smart.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If Harry is quiet then Harry is round.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "round" "+"))
All smart, red things are quiet.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Gary is green.
True
1
proof
[(triple11)]
("Gary" "is" "green" "+")
triple11
Gary is not blue.
False
1
inv-proof
[(triple10)]
("Gary" "is" "blue" "-")
triple10
Harry is round.
True
2
proof
[(((triple14) -> rule2))]
("Harry" "is" "round" "+")
((triple14) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple14) -> rule2))]
("Harry" "is" "round" "-")
((triple14) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
True
4
proof
[(((((triple14) -> rule2) triple14) -> rule1))]
("Harry" "is" "smart" "+")
((((triple14) -> (rule2 % int2)) triple14) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not smart.
False
4
inv-proof
[(((((triple14) -> rule2) triple14) -> rule1))]
("Harry" "is" "smart" "-")
((((triple14) -> (rule2 % int2)) triple14) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "quiet" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Gary is not smart.
Unknown
inv-rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Gary" "is" "smart" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Bob is blue.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3)] Bob is quiet.[(triple4)] Bob is round.[(triple5)] Bob is smart.[(triple6 OR ((triple5 triple4) -> rule1))] Charlie is green.[(triple7)] Charlie is round.[(triple8)] Charlie is smart.[(triple9)] Gary is blue.[(triple10)] Gary is green.[(triple11)] Gary is round.[(triple12)] Harry is kind.[(triple13)] Harry is quiet.[(triple14)] Harry is red.[(triple15)] @1: Harry is round.[(((triple14) -> rule2))] @2: Harry is smart.[(((((triple14) -> rule2) triple14) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple5 triple4) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
triple8
Charlie is smart.
("Charlie" "is" "smart" "+")
triple9
Gary is blue.
("Gary" "is" "blue" "+")
triple10
Gary is green.
("Gary" "is" "green" "+")
triple11
Gary is round.
("Gary" "is" "round" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is red.
("Harry" "is" "red" "+")
triple15
Harry is round.
("Harry" "is" "round" "+")
((triple14) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple14) -> (rule2 % int2)) triple14) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2