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