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