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