Anne is not quiet. Charlie is nice. Dave is quiet. If something is nice then it is red. If Charlie is red and Charlie is nice then Charlie is quiet. Red, nice things are smart. If Dave is quiet then Dave is smart. All quiet things are young. If something is red and not young then it is big.
Anne is not quiet.
("Anne" "is" "quiet" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If Charlie is red and Charlie is nice then Charlie is quiet.
((("Charlie" "is" "red" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "quiet" "+"))
Red, nice things are smart.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If Dave is quiet then Dave is smart.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "smart" "+"))
All quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If something is red and not young then it is big.
((("something" "is" "red" "+") ("something" "is" "young" "~")) -> ("something" "is" "big" "+"))
Anne is not quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Charlie is not nice.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "nice" "-")
triple2
Charlie is red.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "red" "+")
((triple2) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple3) -> rule4))]
("Dave" "is" "smart" "-")
((triple3) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Charlie is smart.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule3))]
("Charlie" "is" "smart" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not quiet.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule2))]
("Charlie" "is" "quiet" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is young.
True
5
proof
[(((((((triple2) -> rule1) triple2) -> rule2)) -> rule5))]
("Charlie" "is" "young" "+")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is not young.
False
5
inv-proof
[(((((((triple2) -> rule1) triple2) -> rule2)) -> rule5))]
("Charlie" "is" "young" "-")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "smart" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "big" "+")
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "big" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "big" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Anne is not quiet.[(triple1)] Charlie is nice.[(triple2)] Dave is quiet.[(triple3)] @1: Charlie is red.[(((triple2) -> rule1))] Dave is smart.[(((triple3) -> rule4))] Dave is young.[(((triple3) -> rule5))] @2: Charlie is quiet.[(((((triple2) -> rule1) triple2) -> rule2))] Charlie is smart.[(((((triple2) -> rule1) triple2) -> rule3))] @3: Charlie is young.[(((((((triple2) -> rule1) triple2) -> rule2)) -> rule5))]
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
((triple2) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple3) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3