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