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