Bob is blue. Bob is smart. Erin is green. Erin is red. Gary is furry. Gary is red. Gary is round. Harry is furry. Harry is green. Harry is smart. All furry things are round. If Bob is red and Bob is smart then Bob is furry. Green things are round. If something is blue and round then it is quiet. Round things are red. If something is green then it is red.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If Bob is red and Bob is smart then Bob is furry.
((("Bob" "is" "red" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "furry" "+"))
Green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something is blue and round then it is quiet.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
Round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is green then it is red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Erin is red.
True
1
proof
[(triple4 OR ((triple3) -> rule6) OR ((((triple3) -> rule3)) -> rule5))]
("Erin" "is" "red" "+")
triple4
((triple3) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Gary is not round.
False
1
inv-proof
[(triple7 OR ((triple5) -> rule1))]
("Gary" "is" "round" "-")
triple7
((triple5) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Bob is not red.
Unknown
inv-rconc
[@4: Bob is red.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule2 <- rule6 <- FAIL)]]
("Bob" "is" "red" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Bob is blue.[(triple1)] Bob is smart.[(triple2)] Erin is green.[(triple3)] Erin is red.[(triple4 OR ((triple3) -> rule6) OR ((((triple3) -> rule3)) -> rule5))] Gary is furry.[(triple5)] Gary is red.[(triple6 OR ((triple7) -> rule5) OR ((((triple5) -> rule1)) -> rule5))] Gary is round.[(triple7 OR ((triple5) -> rule1))] Harry is furry.[(triple8)] Harry is green.[(triple9)] Harry is smart.[(triple10)] @1: Erin is round.[(((triple3) -> rule3))] Harry is red.[(((triple9) -> rule6) OR ((((triple8) -> rule1)) -> rule5) OR ((((triple9) -> rule3)) -> rule5))] Harry is round.[(((triple8) -> rule1) OR ((triple9) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
((triple3) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
((triple7) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple7
((triple5) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
((triple3) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple9) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple8) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple9) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1