Anne is nice. Anne is rough. Charlie is big. Charlie is green. Charlie is kind. Dave is big. Dave is green. Dave is kind. Dave is quiet. Dave is rough. Fiona is green. Fiona is quiet. If something is quiet then it is big. All kind, nice things are rough. All kind things are rough. All kind things are green. If something is nice and green then it is kind. Quiet things are nice.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If something is quiet then it is big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
All kind, nice things are rough.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
All kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is nice and green then it is kind.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
Quiet things are nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
Fiona is green.
True
1
proof
[(triple11)]
("Fiona" "is" "green" "+")
triple11
Dave is not rough.
False
1
inv-proof
[(triple10 OR ((triple8) -> rule3) OR ((triple8 ((triple9) -> rule6)) -> rule2) OR ((((((triple9) -> rule6) triple7) -> rule5)) -> rule3) OR ((((((triple9) -> rule6) triple7) -> rule5) ((triple9) -> rule6)) -> rule2))]
("Dave" "is" "rough" "-")
triple10
((triple8) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple8 ((triple9) -> (rule6 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((((triple9) -> (rule6 % int3)) triple7) -> (rule5 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((((triple9) -> (rule6 % int3)) triple7) -> (rule5 % int2)) ((triple9) -> (rule6 % int3))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Fiona is nice.
True
2
proof
[(((triple12) -> rule6))]
("Fiona" "is" "nice" "+")
((triple12) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not nice.
False
2
inv-proof
[(((triple12) -> rule6))]
("Fiona" "is" "nice" "-")
((triple12) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
True
4
proof
[(((((triple12) -> rule6) triple11) -> rule5))]
("Fiona" "is" "kind" "+")
((((triple12) -> (rule6 % int2)) triple11) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not kind.
False
4
inv-proof
[(((((triple12) -> rule6) triple11) -> rule5))]
("Fiona" "is" "kind" "-")
((((triple12) -> (rule6 % int2)) triple11) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is rough.
True
5
proof
[(((((((triple12) -> rule6) triple11) -> rule5)) -> rule3) OR ((((((triple12) -> rule6) triple11) -> rule5) ((triple12) -> rule6)) -> rule2))]
("Fiona" "is" "rough" "+")
((((((triple12) -> (rule6 % int3)) triple11) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
((((((triple12) -> (rule6 % int3)) triple11) -> (rule5 % int2)) ((triple12) -> (rule6 % int3))) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is not rough.
False
5
inv-proof
[(((((((triple12) -> rule6) triple11) -> rule5)) -> rule3) OR ((((((triple12) -> rule6) triple11) -> rule5) ((triple12) -> rule6)) -> rule2))]
("Fiona" "is" "rough" "-")
((((((triple12) -> (rule6 % int3)) triple11) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
((((((triple12) -> (rule6 % int3)) triple11) -> (rule5 % int2)) ((triple12) -> (rule6 % int3))) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "nice" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not green.
Unknown
inv-rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is kind.
Unknown
rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Anne" "is" "kind" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Anne is nice.[(triple1)] Anne is rough.[(triple2)] Charlie is big.[(triple3)] Charlie is green.[(triple4 OR ((triple5) -> rule4))] Charlie is kind.[(triple5)] Dave is big.[(triple6 OR ((triple9) -> rule1))] Dave is green.[(triple7 OR ((triple8) -> rule4))] Dave is kind.[(triple8 OR ((((triple9) -> rule6) triple7) -> rule5))] Dave is quiet.[(triple9)] Dave is rough.[(triple10 OR ((triple8) -> rule3) OR ((triple8 ((triple9) -> rule6)) -> rule2) OR ((((((triple9) -> rule6) triple7) -> rule5)) -> rule3) OR ((((((triple9) -> rule6) triple7) -> rule5) ((triple9) -> rule6)) -> rule2))] Fiona is green.[(triple11)] Fiona is quiet.[(triple12)] @1: Charlie is rough.[(((triple5) -> rule3))] Dave is nice.[(((triple9) -> rule6))] Fiona is big.[(((triple12) -> rule1))] Fiona is nice.[(((triple12) -> rule6))] @2: Fiona is kind.[(((((triple12) -> rule6) triple11) -> rule5))] @3: Fiona is rough.[(((((((triple12) -> rule6) triple11) -> rule5)) -> rule3) OR ((((((triple12) -> rule6) triple11) -> rule5) ((triple12) -> rule6)) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
((triple5) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
((triple9) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple7
((triple8) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple8
((((triple9) -> (rule6 % int2)) triple7) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
Dave is rough.
("Dave" "is" "rough" "+")
triple10
((triple8) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple8 ((triple9) -> (rule6 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((((triple9) -> (rule6 % int3)) triple7) -> (rule5 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((((triple9) -> (rule6 % int3)) triple7) -> (rule5 % int2)) ((triple9) -> (rule6 % int3))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
triple11
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple12
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple5) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple9) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple12) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple12) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple12) -> (rule6 % int2)) triple11) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((((triple12) -> (rule6 % int3)) triple11) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
((((((triple12) -> (rule6 % int3)) triple11) -> (rule5 % int2)) ((triple12) -> (rule6 % int3))) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3