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