Anne is furry. Charlie is big. Charlie is cold. Charlie is furry. Charlie is young. Dave is big. Dave is cold. Dave is quiet. Erin is big. Erin is kind. Erin is quiet. Erin is smart. If something is smart and furry then it is quiet. If something is cold and young then it is smart. If something is young and smart then it is cold.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If something is smart and furry then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is cold and young then it is smart.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If something is young and smart then it is cold.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Dave is quiet.
True
1
proof
[(triple8)]
("Dave" "is" "quiet" "+")
triple8
Dave is not quiet.
False
1
inv-proof
[(triple8)]
("Dave" "is" "quiet" "-")
triple8
Charlie is smart.
True
3
proof
[(((triple3 triple5) -> rule2))]
("Charlie" "is" "smart" "+")
((triple3 triple5) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
3
inv-proof
[(((triple3 triple5) -> rule2))]
("Charlie" "is" "smart" "-")
((triple3 triple5) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
True
5
proof
[(((((triple3 triple5) -> rule2) triple4) -> rule1))]
("Charlie" "is" "quiet" "+")
((((triple3 triple5) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not quiet.
False
5
inv-proof
[(((((triple3 triple5) -> rule2) triple4) -> rule1))]
("Charlie" "is" "quiet" "-")
((((triple3 triple5) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "cold" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "smart" "+")
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Anne is furry.[(triple1)] Charlie is big.[(triple2)] Charlie is cold.[(triple3)] Charlie is furry.[(triple4)] Charlie is young.[(triple5)] Dave is big.[(triple6)] Dave is cold.[(triple7)] Dave is quiet.[(triple8)] Erin is big.[(triple9)] Erin is kind.[(triple10)] Erin is quiet.[(triple11)] Erin is smart.[(triple12)] @1: Charlie is smart.[(((triple3 triple5) -> rule2))] @2: Charlie is quiet.[(((((triple3 triple5) -> rule2) triple4) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is cold.
("Dave" "is" "cold" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
Erin is big.
("Erin" "is" "big" "+")
triple9
Erin is kind.
("Erin" "is" "kind" "+")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple3 triple5) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple3 triple5) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2