Bob is round. Erin is big. Erin is blue. Erin is furry. Erin is round. Erin is smart. Erin is white. Gary is white. Harry is smart. Harry is white. If someone is smart then they are furry. Furry people are round.
Bob is round.
("Bob" "is" "round" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is smart then they are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
Furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Erin is big.
True
1
proof
[(triple2)]
("Erin" "is" "big" "+")
triple2
Erin is not smart.
False
1
inv-proof
[(triple6)]
("Erin" "is" "smart" "-")
triple6
Harry is furry.
True
2
proof
[(((triple9) -> rule1))]
("Harry" "is" "furry" "+")
((triple9) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple9) -> rule1))]
("Harry" "is" "furry" "-")
((triple9) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
True
3
proof
[(((((triple9) -> rule1)) -> rule2))]
("Harry" "is" "round" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule2))]
("Harry" "is" "round" "-")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Gary is not round.
Unknown
inv-rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "furry" "+")
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "furry" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is round.[(triple1)] Erin is big.[(triple2)] Erin is blue.[(triple3)] Erin is furry.[(triple4 OR ((triple6) -> rule1))] Erin is round.[(triple5 OR ((triple4) -> rule2) OR ((((triple6) -> rule1)) -> rule2))] Erin is smart.[(triple6)] Erin is white.[(triple7)] Gary is white.[(triple8)] Harry is smart.[(triple9)] Harry is white.[(triple10)] @1: Harry is furry.[(((triple9) -> rule1))] @2: Harry is round.[(((((triple9) -> rule1)) -> rule2))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
((triple6) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple5
((triple4) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
Gary is white.
("Gary" "is" "white" "+")
triple8
Harry is smart.
("Harry" "is" "smart" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
((triple9) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2