Bob is quiet. Bob is red. Charlie is furry. Gary is blue. Harry is blue. Harry is quiet. Harry is young. If Charlie is quiet then Charlie is furry. All blue things are round. If something is red and furry then it is quiet. All round, blue things are young. All smart things are young. Young things are blue.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
If Charlie is quiet then Charlie is furry.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "furry" "+"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is red and furry then it is quiet.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
All round, blue things are young.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
Bob is red.
True
1
proof
[(triple2)]
("Bob" "is" "red" "+")
triple2
Harry is not young.
False
1
inv-proof
[(triple7 OR ((((triple5) -> rule2) triple5) -> rule4))]
("Harry" "is" "young" "-")
triple7
((((triple5) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Bob is quiet.[(triple1)] Bob is red.[(triple2)] Charlie is furry.[(triple3)] Gary is blue.[(triple4)] Harry is blue.[(triple5 OR ((triple7) -> rule6))] Harry is quiet.[(triple6)] Harry is young.[(triple7 OR ((((triple5) -> rule2) triple5) -> rule4))] @1: Gary is round.[(((triple4) -> rule2))] Harry is round.[(((triple5) -> rule2) OR ((((triple7) -> rule6)) -> rule2))] @2: Gary is young.[(((((triple4) -> rule2) triple4) -> rule4))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple5
((triple7) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
((((triple5) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple4) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple5) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((triple4) -> (rule2 % int2)) triple4) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2