Bob is big. Bob is not nice. Dave is big. Dave is not blue. Dave is furry. Dave is white. Erin is big. Erin is blue. Erin is green. Erin is nice. Erin is not round. Erin is not white. Harry is blue. Harry is furry. Harry is nice. Harry is round. If someone is white and nice then they are furry. Nice, blue people are furry. All furry people are nice. If Dave is blue and Dave is furry then Dave is green. Nice people are green. If Erin is blue and Erin is not big then Erin is furry.
Bob is big.
("Bob" "is" "big" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not round.
("Erin" "is" "round" "-")
Erin is not white.
("Erin" "is" "white" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is white and nice then they are furry.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Nice, blue people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If Dave is blue and Dave is furry then Dave is green.
((("Dave" "is" "blue" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "green" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If Erin is blue and Erin is not big then Erin is furry.
((("Erin" "is" "blue" "+") ("Erin" "is" "big" "~")) -> ("Erin" "is" "furry" "+"))
Erin is green.
True
1
proof
[(triple9 OR ((triple10) -> rule5))]
("Erin" "is" "green" "+")
triple9
((triple10) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
False
1
inv-proof
[(triple12)]
("Erin" "is" "white" "+")
triple12
Erin is furry.
True
3
proof
[(((triple10 triple8) -> rule2))]
("Erin" "is" "furry" "+")
((triple10 triple8) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple5) -> rule3))]
("Dave" "is" "nice" "-")
((triple5) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
True
3
proof
[(((((triple5) -> rule3)) -> rule5))]
("Dave" "is" "green" "+")
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule5))]
("Dave" "is" "green" "-")
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is furry.
Unknown
rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "furry" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is big.[(triple1)] Bob is not nice.[(triple2)] Dave is big.[(triple3)] Dave is furry.[(triple5)] Dave is not blue.[(triple4)] Dave is white.[(triple6)] Erin is big.[(triple7)] Erin is blue.[(triple8)] Erin is green.[(triple9 OR ((triple10) -> rule5))] Erin is nice.[(triple10)] Erin is not round.[(triple11)] Erin is not white.[(triple12)] Harry is blue.[(triple13)] Harry is furry.[(triple14 OR ((triple15 triple13) -> rule2))] Harry is nice.[(triple15 OR ((triple14) -> rule3))] Harry is round.[(triple16)] @1: Dave is nice.[(((triple5) -> rule3))] Erin is furry.[(((triple10 triple8) -> rule2))] Harry is green.[(((triple15) -> rule5) OR ((((triple14) -> rule3)) -> rule5))] @2: Dave is green.[(((((triple5) -> rule3)) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is not nice.
("Bob" "is" "nice" "-")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is not blue.
("Dave" "is" "blue" "-")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple6
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is green.
("Erin" "is" "green" "+")
triple9
((triple10) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Erin is not round.
("Erin" "is" "round" "-")
triple11
Erin is not white.
("Erin" "is" "white" "-")
triple12
Harry is blue.
("Harry" "is" "blue" "+")
triple13
Harry is furry.
("Harry" "is" "furry" "+")
triple14
((triple15 triple13) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple15
((triple14) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple16
Dave is nice.
("Dave" "is" "nice" "+")
((triple5) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple10 triple8) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple15) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple14) -> (rule3 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2