Charlie is big. Charlie is nice. Dave is cold. Dave is furry. Dave is green. Dave is nice. Dave is rough. If someone is green then they are nice. Rough people are nice. All nice, cold people are furry. If Dave is cold then Dave is big. If someone is rough and cold then they are big. If Dave is green and Dave is cold then Dave is nice. All cold people are big. All cold, furry people are young.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
If someone is green then they are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
All nice, cold people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If Dave is cold then Dave is big.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "big" "+"))
If someone is rough and cold then they are big.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If Dave is green and Dave is cold then Dave is nice.
((("Dave" "is" "green" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "nice" "+"))
All cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
All cold, furry people are young.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Dave is nice.
True
1
proof
[(triple6 OR ((triple5) -> rule1) OR ((triple7) -> rule2) OR ((triple5 triple3) -> rule6))]
("Dave" "is" "nice" "+")
triple6
((triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple7) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple5 triple3) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is big.[(triple1)] Charlie is nice.[(triple2)] Dave is cold.[(triple3)] Dave is furry.[(triple4 OR ((triple6 triple3) -> rule3) OR ((((triple5) -> rule1) triple3) -> rule3) OR ((((triple7) -> rule2) triple3) -> rule3) OR ((((triple5 triple3) -> rule6) triple3) -> rule3))] Dave is green.[(triple5)] Dave is nice.[(triple6 OR ((triple5) -> rule1) OR ((triple7) -> rule2) OR ((triple5 triple3) -> rule6))] Dave is rough.[(triple7)] @1: Dave is big.[(((triple3) -> rule4) OR ((triple3) -> rule7) OR ((triple7 triple3) -> rule5))] Dave is young.[(((triple3 triple4) -> rule8) OR ((triple3 ((triple6 triple3) -> rule3)) -> rule8) OR ((triple3 ((((triple5) -> rule1) triple3) -> rule3)) -> rule8) OR ((triple3 ((((triple7) -> rule2) triple3) -> rule3)) -> rule8) OR ((triple3 ((((triple5 triple3) -> rule6) triple3) -> rule3)) -> rule8))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
((triple6 triple3) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple5) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple7) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple5 triple3) -> (rule6 % int2)) triple3) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
((triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple7) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple5 triple3) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
((triple3) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple3) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple7 triple3) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3 triple4) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple3 ((triple6 triple3) -> (rule3 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((triple3 ((((triple5) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((triple3 ((((triple7) -> (rule2 % int3)) triple3) -> (rule3 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((triple3 ((((triple5 triple3) -> (rule6 % int3)) triple3) -> (rule3 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3