Anne is nice. Anne is round. Charlie is rough. Charlie is round. Dave is nice. Dave is quiet. Dave is not smart. Dave is young. Erin is not quiet. Erin is round. All round things are nice. If something is rough then it is quiet. All quiet things are young.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
Dave is young.
("Dave" "is" "young" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Erin is round.
("Erin" "is" "round" "+")
All round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If something is rough then it is quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
All quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
Dave is nice.
True
1
proof
[(triple5)]
("Dave" "is" "nice" "+")
triple5
Dave is smart.
False
1
inv-proof
[(triple7)]
("Dave" "is" "smart" "+")
triple7
Charlie is nice.
True
2
proof
[(((triple4) -> rule1))]
("Charlie" "is" "nice" "+")
((triple4) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple4) -> rule1))]
("Charlie" "is" "nice" "-")
((triple4) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Charlie" "is" "young" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Charlie" "is" "young" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "young" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not young.
Unknown
inv-rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Anne" "is" "young" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Anne is nice.[(triple1 OR ((triple2) -> rule1))] Anne is round.[(triple2)] Charlie is rough.[(triple3)] Charlie is round.[(triple4)] Dave is nice.[(triple5)] Dave is not smart.[(triple7)] Dave is quiet.[(triple6)] Dave is young.[(triple8 OR ((triple6) -> rule3))] Erin is not quiet.[(triple9)] Erin is round.[(triple10)] @1: Charlie is nice.[(((triple4) -> rule1))] Charlie is quiet.[(((triple3) -> rule2))] Erin is nice.[(((triple10) -> rule1))] @2: Charlie is young.[(((((triple3) -> rule2)) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
((triple2) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is not smart.
("Dave" "is" "smart" "-")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple8
((triple6) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple9
Erin is round.
("Erin" "is" "round" "+")
triple10
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple4) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple10) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2