Dave is kind. Dave is round. Dave is smart. Fiona is round. Gary is kind. Gary is round. Harry is kind. Kind people are green. Round, green people are smart.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Round, green people are smart.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Harry is kind.
True
1
proof
[(triple7)]
("Harry" "is" "kind" "+")
triple7
Fiona is not round.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "round" "-")
triple4
Dave is green.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "green" "+")
((triple1) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple5) -> rule1))]
("Gary" "is" "green" "-")
((triple5) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
True
4
proof
[(((triple6 ((triple5) -> rule1)) -> rule2))]
("Gary" "is" "smart" "+")
((triple6 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not smart.
False
4
inv-proof
[(((triple6 ((triple5) -> rule1)) -> rule2))]
("Gary" "is" "smart" "-")
((triple6 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Fiona is not smart.
Unknown
inv-rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "smart" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "smart" "+")
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "green" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Dave is kind.[(triple1)] Dave is round.[(triple2)] Dave is smart.[(triple3 OR ((triple2 ((triple1) -> rule1)) -> rule2))] Fiona is round.[(triple4)] Gary is kind.[(triple5)] Gary is round.[(triple6)] Harry is kind.[(triple7)] @1: Dave is green.[(((triple1) -> rule1))] Gary is green.[(((triple5) -> rule1))] Harry is green.[(((triple7) -> rule1))] @2: Gary is smart.[(((triple6 ((triple5) -> rule1)) -> rule2))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
((triple2 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
triple4
Gary is kind.
("Gary" "is" "kind" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Dave is green.
("Dave" "is" "green" "+")
((triple1) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple5) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple7) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple6 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2