Bob is blue. Bob is furry. Bob is round. Erin is furry. Erin is nice. Erin is round. Harry is quiet. Kind, blue people are furry. If Harry is smart and Harry is quiet then Harry is round. All furry, nice people are round. Furry people are nice. Furry people are nice. If someone is furry then they are quiet. If Erin is quiet and Erin is nice then Erin is blue. If Bob is furry then Bob is round.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is round.
("Bob" "is" "round" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Kind, blue people are furry.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If Harry is smart and Harry is quiet then Harry is round.
((("Harry" "is" "smart" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "round" "+"))
All furry, nice people are round.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
Furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is furry then they are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If Erin is quiet and Erin is nice then Erin is blue.
((("Erin" "is" "quiet" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "blue" "+"))
If Bob is furry then Bob is round.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "round" "+"))
Erin is round.
True
1
proof
[(triple6 OR ((triple4 triple5) -> rule3) OR ((triple4 ((triple4) -> rule4)) -> rule3) OR ((triple4 ((triple4) -> rule5)) -> rule3))]
("Erin" "is" "round" "+")
triple6
((triple4 triple5) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple4 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple4 ((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Bob is not round.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule8) OR ((triple2 ((triple2) -> rule4)) -> rule3) OR ((triple2 ((triple2) -> rule5)) -> rule3))]
("Bob" "is" "round" "-")
triple3
((triple2) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple2 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is nice.
True
2
proof
[(((triple2) -> rule4) OR ((triple2) -> rule5))]
("Bob" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple2) -> rule6))]
("Bob" "is" "quiet" "-")
((triple2) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Harry is not round.
Unknown
inv-rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Harry" "is" "round" "-")
Harry is furry.
Unknown
rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "furry" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Bob is blue.[(triple1)] Bob is furry.[(triple2)] Bob is round.[(triple3 OR ((triple2) -> rule8) OR ((triple2 ((triple2) -> rule4)) -> rule3) OR ((triple2 ((triple2) -> rule5)) -> rule3))] Erin is furry.[(triple4)] Erin is nice.[(triple5 OR ((triple4) -> rule4) OR ((triple4) -> rule5))] Erin is round.[(triple6 OR ((triple4 triple5) -> rule3) OR ((triple4 ((triple4) -> rule4)) -> rule3) OR ((triple4 ((triple4) -> rule5)) -> rule3))] Harry is quiet.[(triple7)] @1: Bob is nice.[(((triple2) -> rule4) OR ((triple2) -> rule5))] Bob is quiet.[(((triple2) -> rule6))] Erin is quiet.[(((triple4) -> rule6))] @2: Erin is blue.[(((((triple4) -> rule6) triple5) -> rule7) OR ((((triple4) -> rule6) ((triple4) -> rule4)) -> rule7) OR ((((triple4) -> rule6) ((triple4) -> rule5)) -> rule7))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
((triple2) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple2 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Erin is nice.
("Erin" "is" "nice" "+")
triple5
((triple4) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple4) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple6
((triple4 triple5) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple4 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple4 ((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple4) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple4) -> (rule6 % int2)) triple5) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple4) -> (rule6 % int3)) ((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((triple4) -> (rule6 % int3)) ((triple4) -> (rule5 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3