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