Dave is big. Dave is red. Dave is rough. Dave is young. Erin is big. Erin is rough. Erin is round. Gary is furry. Gary is round. Harry is big. Harry is furry. Harry is round. If Erin is red then Erin is rough. If Dave is rough then Dave is blue. All blue people are furry. If someone is big then they are young. Rough people are blue. Round people are young. All rough people are red. If Dave is young then Dave is round.
Dave is big.
("Dave" "is" "big" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is round.
("Harry" "is" "round" "+")
If Erin is red then Erin is rough.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "rough" "+"))
If Dave is rough then Dave is blue.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "blue" "+"))
All blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Rough people are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
Round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
All rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If Dave is young then Dave is round.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "round" "+"))
Dave is red.
True
1
proof
[(triple2 OR ((triple3) -> rule7))]
("Dave" "is" "red" "+")
triple2
((triple3) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Harry is not furry.
False
1
inv-proof
[(triple11)]
("Harry" "is" "furry" "-")
triple11
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "red" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Dave is big.[(triple1)] Dave is red.[(triple2 OR ((triple3) -> rule7))] Dave is rough.[(triple3)] Dave is young.[(triple4 OR ((triple1) -> rule4))] Erin is big.[(triple5)] Erin is rough.[(triple6)] Erin is round.[(triple7)] Gary is furry.[(triple8)] Gary is round.[(triple9)] Harry is big.[(triple10)] Harry is furry.[(triple11)] Harry is round.[(triple12)] @1: Dave is blue.[(((triple3) -> rule2) OR ((triple3) -> rule5))] Dave is round.[(((triple4) -> rule8) OR ((((triple1) -> rule4)) -> rule8))] Erin is blue.[(((triple6) -> rule5))] Erin is red.[(((triple6) -> rule7))] Erin is young.[(((triple5) -> rule4) OR ((triple7) -> rule6))] Gary is young.[(((triple9) -> rule6))] Harry is young.[(((triple10) -> rule4) OR ((triple12) -> rule6))] @2: Dave is furry.[(((((triple3) -> rule2)) -> rule3) OR ((((triple3) -> rule5)) -> rule3))] Erin is furry.[(((((triple6) -> rule5)) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
((triple3) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
((triple1) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is rough.
("Erin" "is" "rough" "+")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Dave is blue.
("Dave" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple3) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple4) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((triple6) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple6) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple5) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple7) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple9) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple10) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple12) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2