Anne is nice. Charlie is blue. Erin is blue. Fiona is big. All smart, green people are blue. Quiet people are smart. Big people are quiet. Blue people are green. If someone is smart and quiet then they are green. If someone is red and big then they are green.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Fiona is big.
("Fiona" "is" "big" "+")
All smart, green people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
Blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If someone is smart and quiet then they are green.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If someone is red and big then they are green.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Erin is blue.
True
1
proof
[(triple3)]
("Erin" "is" "blue" "+")
triple3
Erin is not blue.
False
1
inv-proof
[(triple3)]
("Erin" "is" "blue" "-")
triple3
Charlie is green.
True
2
proof
[(((triple2) -> rule4))]
("Charlie" "is" "green" "+")
((triple2) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Fiona is not quiet.
False
2
inv-proof
[(((triple4) -> rule3))]
("Fiona" "is" "quiet" "-")
((triple4) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("Fiona" "is" "smart" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is not smart.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("Fiona" "is" "smart" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is green.
True
6
proof
[(((((((triple4) -> rule3)) -> rule2) ((triple4) -> rule3)) -> rule5))]
("Fiona" "is" "green" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2)) ((triple4) -> (rule3 % int3))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is not green.
False
6
inv-proof
[(((((((triple4) -> rule3)) -> rule2) ((triple4) -> rule3)) -> rule5))]
("Fiona" "is" "green" "-")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2)) ((triple4) -> (rule3 % int3))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Anne is blue.
Unknown
rconc
[@3: Anne is blue.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule3 <- FAIL)]]
("Anne" "is" "blue" "+")
Erin is not smart.
Unknown
inv-rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Erin" "is" "smart" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is nice.[(triple1)] Charlie is blue.[(triple2)] Erin is blue.[(triple3)] Fiona is big.[(triple4)] @1: Charlie is green.[(((triple2) -> rule4))] Erin is green.[(((triple3) -> rule4))] Fiona is quiet.[(((triple4) -> rule3))] @2: Fiona is smart.[(((((triple4) -> rule3)) -> rule2))] @3: Fiona is green.[(((((((triple4) -> rule3)) -> rule2) ((triple4) -> rule3)) -> rule5))] @4: Fiona is blue.[(((((((triple4) -> rule3)) -> rule2) ((((((triple4) -> rule3)) -> rule2) ((triple4) -> rule3)) -> rule5)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
Charlie is green.
("Charlie" "is" "green" "+")
((triple2) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple4) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2)) ((triple4) -> (rule3 % int3))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
((((((triple4) -> (rule3 % int4))) -> (rule2 % int3)) ((((((triple4) -> (rule3 % int4))) -> (rule2 % int3)) ((triple4) -> (rule3 % int4))) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4