Dave is green. Dave is kind. Dave is quiet. Dave is round. Dave is white. Dave is young. Fiona is kind. Fiona is not quiet. Fiona is round. Fiona is white. White, smart things are kind. If something is quiet then it is smart. If something is kind and not white then it is young.
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
White, smart things are kind.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
If something is quiet then it is smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If something is kind and not white then it is young.
((("something" "is" "kind" "+") ("something" "is" "white" "~")) -> ("something" "is" "young" "+"))
Dave is kind.
True
1
proof
[(triple2 OR ((triple5 ((triple3) -> rule2)) -> rule1))]
("Dave" "is" "kind" "+")
triple2
((triple5 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Fiona is not white.
False
1
inv-proof
[(triple10)]
("Fiona" "is" "white" "-")
triple10
Dave is smart.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "smart" "-")
((triple3) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "young" "+")
@0: Dave is green.[(triple1)] Dave is kind.[(triple2 OR ((triple5 ((triple3) -> rule2)) -> rule1))] Dave is quiet.[(triple3)] Dave is round.[(triple4)] Dave is white.[(triple5)] Dave is young.[(triple6)] Fiona is kind.[(triple7)] Fiona is not quiet.[(triple8)] Fiona is round.[(triple9)] Fiona is white.[(triple10)] @1: Dave is smart.[(((triple3) -> rule2))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
((triple5 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
Fiona is kind.
("Fiona" "is" "kind" "+")
triple7
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
triple8
Fiona is round.
("Fiona" "is" "round" "+")
triple9
Fiona is white.
("Fiona" "is" "white" "+")
triple10
Dave is smart.
("Dave" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1