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