Bob is blue. Bob is nice. Dave is big. Erin is big. Harry is not blue. Harry is round. Harry is white. All big people are round. Big people are furry. If someone is big then they are green. All round people are nice. If someone is round then they are not blue. If Bob is green and Bob is not blue then Bob is furry. If someone is nice and not blue then they are white. If someone is furry and not green then they are not white.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is big.
("Dave" "is" "big" "+")
Erin is big.
("Erin" "is" "big" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
All big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Big people are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
If someone is big then they are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone is round then they are not blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "-"))
If Bob is green and Bob is not blue then Bob is furry.
((("Bob" "is" "green" "+") ("Bob" "is" "blue" "~")) -> ("Bob" "is" "furry" "+"))
If someone is nice and not blue then they are white.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "white" "+"))
If someone is furry and not green then they are not white.
((("someone" "is" "furry" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "white" "-"))
Dave is big.
True
1
proof
[(triple3)]
("Dave" "is" "big" "+")
triple3
Harry is not white.
False
1
inv-proof
[(triple7 OR ((((triple6) -> rule4) triple5) -> rule7) OR ((((triple6) -> rule4) ((triple6) -> rule5)) -> rule7))]
("Harry" "is" "white" "-")
triple7
((((triple6) -> (rule4 % int2)) triple5) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple6) -> (rule4 % int3)) ((triple6) -> (rule5 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Dave is round.
True
2
proof
[(((triple3) -> rule1))]
("Dave" "is" "round" "+")
((triple3) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple3) -> rule3))]
("Dave" "is" "green" "-")
((triple3) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Erin is not blue.
True
3
proof
[(((((triple4) -> rule1)) -> rule5))]
("Erin" "is" "blue" "-")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Dave is not nice.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule4))]
("Dave" "is" "nice" "-")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Erin is white.
True
7
proof
[(((((((triple4) -> rule1)) -> rule4) ((((triple4) -> rule1)) -> rule5)) -> rule7))]
("Erin" "is" "white" "+")
((((((triple4) -> (rule1 % int4))) -> (rule4 % int3)) ((((triple4) -> (rule1 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not blue.
("Erin" "is" "blue" "-")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Dave is not white.
False
7
inv-proof
[(((((((triple3) -> rule1)) -> rule4) ((((triple3) -> rule1)) -> rule5)) -> rule7))]
("Dave" "is" "white" "-")
((((((triple3) -> (rule1 % int4))) -> (rule4 % int3)) ((((triple3) -> (rule1 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "green" "+")
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "furry" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "green" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is blue.[(triple1)] Bob is nice.[(triple2)] Dave is big.[(triple3)] Erin is big.[(triple4)] Harry is not blue.[(triple5 OR ((triple6) -> rule5))] Harry is round.[(triple6)] Harry is white.[(triple7 OR ((((triple6) -> rule4) triple5) -> rule7) OR ((((triple6) -> rule4) ((triple6) -> rule5)) -> rule7))] @1: Dave is furry.[(((triple3) -> rule2))] Dave is green.[(((triple3) -> rule3))] Dave is round.[(((triple3) -> rule1))] Erin is furry.[(((triple4) -> rule2))] Erin is green.[(((triple4) -> rule3))] Erin is round.[(((triple4) -> rule1))] Harry is nice.[(((triple6) -> rule4))] @2: Dave is nice.[(((((triple3) -> rule1)) -> rule4))] Dave is not blue.[(((((triple3) -> rule1)) -> rule5))] Erin is nice.[(((((triple4) -> rule1)) -> rule4))] Erin is not blue.[(((((triple4) -> rule1)) -> rule5))] @3: Dave is white.[(((((((triple3) -> rule1)) -> rule4) ((((triple3) -> rule1)) -> rule5)) -> rule7))] Erin is white.[(((((((triple4) -> rule1)) -> rule4) ((((triple4) -> rule1)) -> rule5)) -> rule7))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Harry is not blue.
("Harry" "is" "blue" "-")
triple5
((triple6) -> (rule5 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
((((triple6) -> (rule4 % int2)) triple5) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple6) -> (rule4 % int3)) ((triple6) -> (rule5 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((triple3) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple3) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple3) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple4) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple4) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple4) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple6) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not blue.
("Dave" "is" "blue" "-")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((((triple3) -> (rule1 % int4))) -> (rule4 % int3)) ((((triple3) -> (rule1 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
((((((triple4) -> (rule1 % int4))) -> (rule4 % int3)) ((((triple4) -> (rule1 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not blue.
("Erin" "is" "blue" "-")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4