Charlie is cold. Charlie is rough. Dave is cold. Dave is furry. Dave is green. Dave is kind. Dave is nice. Dave is round. Fiona is nice. Fiona is round. Gary is cold. Gary is round. If someone is green and nice then they are kind. Furry people are green. Cold, green people are furry. If Gary is nice then Gary is kind. If Charlie is round then Charlie is cold. All round people are rough. All kind people are furry. If someone is cold then they are nice.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
If someone is green and nice then they are kind.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
Furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
Cold, green people are furry.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If Gary is nice then Gary is kind.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "kind" "+"))
If Charlie is round then Charlie is cold.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "cold" "+"))
All round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All kind people are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
If someone is cold then they are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
Dave is furry.
True
1
proof
[(triple4 OR ((triple6) -> rule7) OR ((triple3 triple5) -> rule3) OR ((((triple5 triple7) -> rule1)) -> rule7) OR ((((triple5 ((triple3) -> rule8)) -> rule1)) -> rule7))]
("Dave" "is" "furry" "+")
triple4
((triple6) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple3 triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple5 triple7) -> (rule1 % int2))) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple5 ((triple3) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Gary is not cold.
False
1
inv-proof
[(triple11)]
("Gary" "is" "cold" "-")
triple11
Gary is rough.
True
2
proof
[(((triple12) -> rule6))]
("Gary" "is" "rough" "+")
((triple12) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple8) -> rule6))]
("Dave" "is" "rough" "-")
((triple8) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Gary is kind.
True
3
proof
[(((((triple11) -> rule8)) -> rule4))]
("Gary" "is" "kind" "+")
((((triple11) -> (rule8 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not kind.
False
3
inv-proof
[(((((triple11) -> rule8)) -> rule4))]
("Gary" "is" "kind" "-")
((((triple11) -> (rule8 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is furry.
True
4
proof
[(((((((triple11) -> rule8)) -> rule4)) -> rule7))]
("Gary" "is" "furry" "+")
((((((triple11) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is not furry.
False
4
inv-proof
[(((((((triple11) -> rule8)) -> rule4)) -> rule7))]
("Gary" "is" "furry" "-")
((((((triple11) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Fiona is not kind.
Unknown
inv-rconc
[@3: Fiona is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule3 <- FAIL)]]
("Fiona" "is" "kind" "-")
Charlie is furry.
Unknown
rconc
[@4: Charlie is furry.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule7 <- rule1 <- FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not kind.
Unknown
inv-rconc
[@3: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule3 <- FAIL)]]
("Charlie" "is" "kind" "-")
Fiona is green.
Unknown
rconc
[@3: Fiona is green.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule1 <- FAIL)]]
("Fiona" "is" "green" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is cold.[(triple1)] Charlie is rough.[(triple2)] Dave is cold.[(triple3)] Dave is furry.[(triple4 OR ((triple6) -> rule7) OR ((triple3 triple5) -> rule3) OR ((((triple5 triple7) -> rule1)) -> rule7) OR ((((triple5 ((triple3) -> rule8)) -> rule1)) -> rule7))] Dave is green.[(triple5 OR ((triple4) -> rule2) OR ((((triple6) -> rule7)) -> rule2))] Dave is kind.[(triple6 OR ((triple5 triple7) -> rule1) OR ((triple5 ((triple3) -> rule8)) -> rule1) OR ((((triple4) -> rule2) triple7) -> rule1) OR ((((triple4) -> rule2) ((triple3) -> rule8)) -> rule1))] Dave is nice.[(triple7 OR ((triple3) -> rule8))] Dave is round.[(triple8)] Fiona is nice.[(triple9)] Fiona is round.[(triple10)] Gary is cold.[(triple11)] Gary is round.[(triple12)] @1: Charlie is nice.[(((triple1) -> rule8))] Dave is rough.[(((triple8) -> rule6))] Fiona is rough.[(((triple10) -> rule6))] Gary is nice.[(((triple11) -> rule8))] Gary is rough.[(((triple12) -> rule6))] @2: Gary is kind.[(((((triple11) -> rule8)) -> rule4))] @3: Gary is furry.[(((((((triple11) -> rule8)) -> rule4)) -> rule7))] @4: Gary is green.[(((((((((triple11) -> rule8)) -> rule4)) -> rule7)) -> rule2))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
((triple6) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple3 triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple5 triple7) -> (rule1 % int2))) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple5 ((triple3) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
triple5
((triple4) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple6
((triple5 triple7) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple5 ((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple4) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple4) -> (rule2 % int3)) ((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
triple7
((triple3) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple8
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
Gary is cold.
("Gary" "is" "cold" "+")
triple11
Gary is round.
("Gary" "is" "round" "+")
triple12
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple8) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple10) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple11) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple12) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((((triple11) -> (rule8 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((((triple11) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((((((((triple11) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4