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