Dave is big. Fiona is kind. Fiona is smart. Gary is big. Gary is not furry. Gary is smart. Harry is kind. If Gary is smart then Gary is blue. Blue, smart things are quiet.
Dave is big.
("Dave" "is" "big" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If Gary is smart then Gary is blue.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "blue" "+"))
Blue, smart things are quiet.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Harry is kind.
True
1
proof
[(triple7)]
("Harry" "is" "kind" "+")
triple7
Harry is not kind.
False
1
inv-proof
[(triple7)]
("Harry" "is" "kind" "-")
triple7
Gary is blue.
True
2
proof
[(((triple6) -> rule1))]
("Gary" "is" "blue" "+")
((triple6) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple6) -> rule1))]
("Gary" "is" "blue" "-")
((triple6) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
True
4
proof
[(((((triple6) -> rule1) triple6) -> rule2))]
("Gary" "is" "quiet" "+")
((((triple6) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not quiet.
False
4
inv-proof
[(((((triple6) -> rule1) triple6) -> rule2))]
("Gary" "is" "quiet" "-")
((((triple6) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "quiet" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "quiet" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Dave is big.[(triple1)] Fiona is kind.[(triple2)] Fiona is smart.[(triple3)] Gary is big.[(triple4)] Gary is not furry.[(triple5)] Gary is smart.[(triple6)] Harry is kind.[(triple7)] @1: Gary is blue.[(((triple6) -> rule1))] @2: Gary is quiet.[(((((triple6) -> rule1) triple6) -> rule2))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Gary is not furry.
("Gary" "is" "furry" "-")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
((triple6) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple6) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2