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