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