Anne is nice. Anne is quiet. Anne is smart. Anne is young. Charlie is furry. Charlie is nice. Charlie is round. Charlie is smart. Dave is kind. Dave is nice. Dave is quiet. Dave is young. Erin is furry. Erin is quiet. Erin is round. Erin is young. If something is young and kind then it is nice. If something is nice and quiet then it is kind. If something is kind then it is quiet. If something is furry and smart then it is nice. If Dave is furry and Dave is quiet then Dave is young. If Anne is smart then Anne is young. All quiet, smart things are round. All nice, round things are kind.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is young and kind then it is nice.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is nice and quiet then it is kind.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it is quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If something is furry and smart then it is nice.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If Dave is furry and Dave is quiet then Dave is young.
((("Dave" "is" "furry" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "young" "+"))
If Anne is smart then Anne is young.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "young" "+"))
All quiet, smart things are round.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
All nice, round things are kind.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Erin is quiet.
True
1
proof
[(triple14)]
("Erin" "is" "quiet" "+")
triple14
Erin is not round.
False
1
inv-proof
[(triple15)]
("Erin" "is" "round" "-")
triple15
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Anne is nice.[(triple1)] Anne is quiet.[(triple2)] Anne is smart.[(triple3)] Anne is young.[(triple4 OR ((triple3) -> rule6))] Charlie is furry.[(triple5)] Charlie is nice.[(triple6 OR ((triple5 triple8) -> rule4))] Charlie is round.[(triple7)] Charlie is smart.[(triple8)] Dave is kind.[(triple9 OR ((triple10 triple11) -> rule2))] Dave is nice.[(triple10 OR ((triple12 triple9) -> rule1))] Dave is quiet.[(triple11 OR ((triple9) -> rule3))] Dave is young.[(triple12)] Erin is furry.[(triple13)] Erin is quiet.[(triple14)] Erin is round.[(triple15)] Erin is young.[(triple16)] @1: Anne is kind.[(((triple1 triple2) -> rule2) OR ((triple1 ((triple2 triple3) -> rule7)) -> rule8))] Anne is round.[(((triple2 triple3) -> rule7))] Charlie is kind.[(((triple6 triple7) -> rule8) OR ((((triple5 triple8) -> rule4) triple7) -> rule8))] @2: Charlie is quiet.[(((((triple6 triple7) -> rule8)) -> rule3) OR ((((((triple5 triple8) -> rule4) triple7) -> rule8)) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
((triple3) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
((triple5 triple8) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
Dave is kind.
("Dave" "is" "kind" "+")
triple9
((triple10 triple11) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple10
((triple12 triple9) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple11
((triple9) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple12
Erin is furry.
("Erin" "is" "furry" "+")
triple13
Erin is quiet.
("Erin" "is" "quiet" "+")
triple14
Erin is round.
("Erin" "is" "round" "+")
triple15
Erin is young.
("Erin" "is" "young" "+")
triple16
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple1 ((triple2 triple3) -> (rule7 % int2))) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((triple2 triple3) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple6 triple7) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple5 triple8) -> (rule4 % int2)) triple7) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple6 triple7) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple5 triple8) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3