Anne is nice. Charlie is big. Charlie is nice. Charlie is quiet. Dave is smart. Erin is not furry. Erin is nice. All cold people are big. Round people are cold. All furry people are cold. Cold people are round. All smart people are round. Smart people are not quiet.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is nice.
("Erin" "is" "nice" "+")
All cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
Round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
All furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
All smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Smart people are not quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "-"))
Erin is nice.
True
1
proof
[(triple7)]
("Erin" "is" "nice" "+")
triple7
Charlie is not nice.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "nice" "-")
triple3
Dave is round.
True
2
proof
[(((triple5) -> rule5))]
("Dave" "is" "round" "+")
((triple5) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple5) -> rule5))]
("Dave" "is" "round" "-")
((triple5) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
True
3
proof
[(((((triple5) -> rule5)) -> rule2))]
("Dave" "is" "cold" "+")
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not cold.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule2))]
("Dave" "is" "cold" "-")
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
True
4
proof
[(((((((triple5) -> rule5)) -> rule2)) -> rule1))]
("Dave" "is" "big" "+")
((((((triple5) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is not big.
False
4
inv-proof
[(((((((triple5) -> rule5)) -> rule2)) -> rule1))]
("Dave" "is" "big" "-")
((((((triple5) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Charlie is not round.
Unknown
inv-rconc
[@3: Charlie is round.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule5 <- FAIL)]]
("Charlie" "is" "round" "-")
Erin is cold.
Unknown
rconc
[@3: Erin is cold.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule3 <- FAIL)]]
("Erin" "is" "cold" "+")
Anne is not round.
Unknown
inv-rconc
[@3: Anne is round.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule5 <- FAIL)]]
("Anne" "is" "round" "-")
Charlie is cold.
Unknown
rconc
[@3: Charlie is cold.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule3 <- FAIL)]]
("Charlie" "is" "cold" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Anne is nice.[(triple1)] Charlie is big.[(triple2)] Charlie is nice.[(triple3)] Charlie is quiet.[(triple4)] Dave is smart.[(triple5)] Erin is nice.[(triple7)] Erin is not furry.[(triple6)] @1: Dave is not quiet.[(((triple5) -> rule6))] Dave is round.[(((triple5) -> rule5))] @2: Dave is cold.[(((((triple5) -> rule5)) -> rule2))] @3: Dave is big.[(((((((triple5) -> rule5)) -> rule2)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple7
Erin is not furry.
("Erin" "is" "furry" "-")
triple6
Dave is not quiet.
("Dave" "is" "quiet" "-")
((triple5) -> (rule6 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple5) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple5) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3