Anne is red. Charlie is round. Dave is round. Fiona is smart. Smart people are not blue. If someone is smart and not blue then they are nice. If someone is nice then they are red.
Anne is red.
("Anne" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Smart people are not blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "-"))
If someone is smart and not blue then they are nice.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Fiona is not smart.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "smart" "-")
triple4
Fiona is not blue.
True
2
proof
[(((triple4) -> rule1))]
("Fiona" "is" "blue" "-")
((triple4) -> (rule1 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is blue.
False
2
inv-proof
[(((triple4) -> rule1))]
("Fiona" "is" "blue" "+")
((triple4) -> (rule1 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is nice.
True
4
proof
[(((triple4 ((triple4) -> rule1)) -> rule2))]
("Fiona" "is" "nice" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not blue.
("Fiona" "is" "blue" "-")
int2
Fiona is not nice.
False
4
inv-proof
[(((triple4 ((triple4) -> rule1)) -> rule2))]
("Fiona" "is" "nice" "-")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not blue.
("Fiona" "is" "blue" "-")
int2
Fiona is red.
True
5
proof
[(((((triple4 ((triple4) -> rule1)) -> rule2)) -> rule3))]
("Fiona" "is" "red" "+")
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not blue.
("Fiona" "is" "blue" "-")
int3
Fiona is not red.
False
5
inv-proof
[(((((triple4 ((triple4) -> rule1)) -> rule2)) -> rule3))]
("Fiona" "is" "red" "-")
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not blue.
("Fiona" "is" "blue" "-")
int3
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "nice" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "nice" "+")
Charlie is not red.
Unknown
inv-rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "red" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "nice" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is red.[(triple1)] Charlie is round.[(triple2)] Dave is round.[(triple3)] Fiona is smart.[(triple4)] @1: Fiona is not blue.[(((triple4) -> rule1))] @2: Fiona is nice.[(((triple4 ((triple4) -> rule1)) -> rule2))] @3: Fiona is red.[(((((triple4 ((triple4) -> rule1)) -> rule2)) -> rule3))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple4
Fiona is not blue.
("Fiona" "is" "blue" "-")
((triple4) -> (rule1 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not blue.
("Fiona" "is" "blue" "-")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not blue.
("Fiona" "is" "blue" "-")
int3