Charlie is quiet. Fiona is furry. Quiet things are round. If Charlie is quiet and Charlie is round then Charlie is red. If something is white then it is round. If something is kind then it is red. If Fiona is white and Fiona is quiet then Fiona is red. If something is red and blue then it is quiet. If Charlie is quiet then Charlie is furry. If something is red then it is blue.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If Charlie is quiet and Charlie is round then Charlie is red.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "red" "+"))
If something is white then it is round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
If something is kind then it is red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If Fiona is white and Fiona is quiet then Fiona is red.
((("Fiona" "is" "white" "+") ("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "red" "+"))
If something is red and blue then it is quiet.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is quiet then Charlie is furry.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "furry" "+"))
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Charlie is quiet.
True
1
proof
[(triple1)]
("Charlie" "is" "quiet" "+")
triple1
Charlie is not quiet.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "quiet" "-")
triple1
Charlie is round.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "round" "+")
((triple1) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "round" "-")
((triple1) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("Charlie" "is" "red" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not red.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("Charlie" "is" "red" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is blue.
True
5
proof
[(((((triple1 ((triple1) -> rule1)) -> rule2)) -> rule8))]
("Charlie" "is" "blue" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is not blue.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule2)) -> rule8))]
("Charlie" "is" "blue" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Fiona is not quiet.
Unknown
inv-rconc
[@2: Fiona is quiet.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not blue.
Unknown
inv-rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is round.
Unknown
rconc
[@3: Fiona is round.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule4 <- FAIL)]]
("Fiona" "is" "round" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Charlie is quiet.[(triple1)] Fiona is furry.[(triple2)] @1: Charlie is furry.[(((triple1) -> rule7))] Charlie is round.[(((triple1) -> rule1))] @2: Charlie is red.[(((triple1 ((triple1) -> rule1)) -> rule2))] @3: Charlie is blue.[(((((triple1 ((triple1) -> rule1)) -> rule2)) -> rule8))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3