Charlie is blue. Charlie is furry. Charlie is kind. Charlie is red. Charlie is rough. Charlie is round. Charlie is not white. Dave is blue. Dave is not furry. Dave is kind. Dave is red. Dave is round. Fiona is blue. Fiona is furry. Fiona is rough. If Dave is kind then Dave is not white. If someone is white and kind then they are red. If Charlie is rough and Charlie is not white then Charlie is furry. All round, red people are rough. All furry people are round. Furry people are kind.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If Dave is kind then Dave is not white.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "white" "-"))
If someone is white and kind then they are red.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If Charlie is rough and Charlie is not white then Charlie is furry.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "white" "~")) -> ("Charlie" "is" "furry" "+"))
All round, red people are rough.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
All furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Charlie is kind.
True
1
proof
[(triple3 OR ((triple2) -> rule6) OR ((((triple5 triple7) -> rule3)) -> rule6) OR ((((((triple6 triple4) -> rule4) triple7) -> rule3)) -> rule6))]
("Charlie" "is" "kind" "+")
triple3
((triple2) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple5 triple7) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((((triple6 triple4) -> (rule4 % int3)) triple7) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not red.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "red" "-")
triple4
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Charlie is blue.[(triple1)] Charlie is furry.[(triple2 OR ((triple5 triple7) -> rule3) OR ((((triple6 triple4) -> rule4) triple7) -> rule3))] Charlie is kind.[(triple3 OR ((triple2) -> rule6) OR ((((triple5 triple7) -> rule3)) -> rule6) OR ((((((triple6 triple4) -> rule4) triple7) -> rule3)) -> rule6))] Charlie is not white.[(triple7)] Charlie is red.[(triple4)] Charlie is rough.[(triple5 OR ((triple6 triple4) -> rule4) OR ((((triple2) -> rule5) triple4) -> rule4))] Charlie is round.[(triple6 OR ((triple2) -> rule5) OR ((((triple5 triple7) -> rule3)) -> rule5))] Dave is blue.[(triple8)] Dave is kind.[(triple10)] Dave is not furry.[(triple9)] Dave is red.[(triple11)] Dave is round.[(triple12)] Fiona is blue.[(triple13)] Fiona is furry.[(triple14)] Fiona is rough.[(triple15)] @1: Dave is not white.[(((triple10) -> rule1))] Dave is rough.[(((triple12 triple11) -> rule4))] Fiona is kind.[(((triple14) -> rule6))] Fiona is round.[(((triple14) -> rule5))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
((triple5 triple7) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple6 triple4) -> (rule4 % int2)) triple7) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple2) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple5 triple7) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((((triple6 triple4) -> (rule4 % int3)) triple7) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not white.
("Charlie" "is" "white" "-")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
((triple6 triple4) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple2) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple6
((triple2) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple5 triple7) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Dave is not furry.
("Dave" "is" "furry" "-")
triple9
Dave is red.
("Dave" "is" "red" "+")
triple11
Dave is round.
("Dave" "is" "round" "+")
triple12
Fiona is blue.
("Fiona" "is" "blue" "+")
triple13
Fiona is furry.
("Fiona" "is" "furry" "+")
triple14
Fiona is rough.
("Fiona" "is" "rough" "+")
triple15
Dave is not white.
("Dave" "is" "white" "-")
((triple10) -> (rule1 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple12 triple11) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple14) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple14) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1