Anne is nice. Anne is red. Charlie is big. Charlie is red. Erin is blue. Fiona is blue. Fiona is not nice. Smart, big things are not nice. All quiet, smart things are nice. Nice things are quiet. If Anne is smart then Anne is big. If something is big and not red then it is blue. Rough things are blue. If Charlie is not red then Charlie is big. Quiet things are rough.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is not nice.
("Fiona" "is" "nice" "-")
Smart, big things are not nice.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "-"))
All quiet, smart things are nice.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If Anne is smart then Anne is big.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "big" "+"))
If something is big and not red then it is blue.
((("something" "is" "big" "+") ("something" "is" "red" "~")) -> ("something" "is" "blue" "+"))
Rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If Charlie is not red then Charlie is big.
((("Charlie" "is" "red" "~")) -> ("Charlie" "is" "big" "+"))
Quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Fiona is not nice.
True
1
proof
[(triple7)]
("Fiona" "is" "nice" "-")
triple7
Charlie is not big.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "big" "-")
triple3
Anne is quiet.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
True
3
proof
[(((((triple1) -> rule3)) -> rule8))]
("Anne" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not rough.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule8))]
("Anne" "is" "rough" "-")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is blue.
True
4
proof
[(((((((triple1) -> rule3)) -> rule8)) -> rule6))]
("Anne" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not blue.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule8)) -> rule6))]
("Anne" "is" "blue" "-")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "nice" "-")
Fiona is quiet.
Unknown
rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is quiet.
Unknown
rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Anne is nice.[(triple1)] Anne is red.[(triple2)] Charlie is big.[(triple3)] Charlie is red.[(triple4)] Erin is blue.[(triple5)] Fiona is blue.[(triple6)] Fiona is not nice.[(triple7)] @1: Anne is quiet.[(((triple1) -> rule3))] @2: Anne is rough.[(((((triple1) -> rule3)) -> rule8))] @3: Anne is blue.[(((((((triple1) -> rule3)) -> rule8)) -> rule6))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
Fiona is not nice.
("Fiona" "is" "nice" "-")
triple7
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3