Anne is kind. Anne is nice. Anne is round. Dave is nice. Dave is round. Dave is white. Erin is nice. Erin is smart. Erin is white. Fiona is furry. Fiona is smart. Fiona is white. All white people are young. All furry, white people are smart. Young, kind people are smart. If someone is round and not furry then they are white. All nice people are white. If someone is kind then they are round.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
All white people are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
All furry, white people are smart.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
Young, kind people are smart.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is round and not furry then they are white.
((("someone" "is" "round" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "white" "+"))
All nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If someone is kind then they are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Dave is white.
True
1
proof
[(triple6 OR ((triple4) -> rule5))]
("Dave" "is" "white" "+")
triple6
((triple4) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is not furry.
False
1
inv-proof
[(triple10)]
("Fiona" "is" "furry" "-")
triple10
Fiona is young.
True
2
proof
[(((triple12) -> rule1))]
("Fiona" "is" "young" "+")
((triple12) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple2) -> rule5))]
("Anne" "is" "white" "-")
((triple2) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("Anne" "is" "young" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("Anne" "is" "young" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
True
5
proof
[(((((((triple2) -> rule5)) -> rule1) triple1) -> rule3))]
("Anne" "is" "smart" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not smart.
False
5
inv-proof
[(((((((triple2) -> rule5)) -> rule1) triple1) -> rule3))]
("Anne" "is" "smart" "-")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "smart" "-")
Erin is round.
Unknown
rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "round" "+")
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "round" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Anne is nice.[(triple2)] Anne is round.[(triple3 OR ((triple1) -> rule6))] Dave is nice.[(triple4)] Dave is round.[(triple5)] Dave is white.[(triple6 OR ((triple4) -> rule5))] Erin is nice.[(triple7)] Erin is smart.[(triple8)] Erin is white.[(triple9 OR ((triple7) -> rule5))] Fiona is furry.[(triple10)] Fiona is smart.[(triple11 OR ((triple10 triple12) -> rule2))] Fiona is white.[(triple12)] @1: Anne is white.[(((triple2) -> rule5))] Dave is young.[(((triple6) -> rule1) OR ((((triple4) -> rule5)) -> rule1))] Erin is young.[(((triple9) -> rule1) OR ((((triple7) -> rule5)) -> rule1))] Fiona is young.[(((triple12) -> rule1))] @2: Anne is young.[(((((triple2) -> rule5)) -> rule1))] @3: Anne is smart.[(((((((triple2) -> rule5)) -> rule1) triple1) -> rule3))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
((triple1) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple4) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
triple8
Erin is white.
("Erin" "is" "white" "+")
triple9
((triple7) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple10
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
((triple10 triple12) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple12
Anne is white.
("Anne" "is" "white" "+")
((triple2) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple6) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((triple9) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((triple12) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3