Bob is cold. Erin is nice. Gary is nice. Harry is blue. Blue people are furry. Nice people are furry. Blue, big people are nice. If someone is cold then they are quiet. All nice, furry people are cold. If Gary is nice then Gary is smart. Cold people are furry. Cold, furry people are quiet.
Bob is cold.
("Bob" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Blue, big people are nice.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold then they are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
All nice, furry people are cold.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If Gary is nice then Gary is smart.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "smart" "+"))
Cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Cold, furry people are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Erin is nice.
True
1
proof
[(triple2)]
("Erin" "is" "nice" "+")
triple2
Gary is not nice.
False
1
inv-proof
[(triple3)]
("Gary" "is" "nice" "-")
triple3
Gary is furry.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "furry" "+")
((triple3) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "furry" "-")
((triple2) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
True
4
proof
[(((triple2 ((triple2) -> rule2)) -> rule5))]
("Erin" "is" "cold" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not cold.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule5))]
("Erin" "is" "cold" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Gary is quiet.
True
5
proof
[(((((triple3 ((triple3) -> rule2)) -> rule5)) -> rule4) OR ((((triple3 ((triple3) -> rule2)) -> rule5) ((triple3) -> rule2)) -> rule8))]
("Gary" "is" "quiet" "+")
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule5 % int2)) ((triple3) -> (rule2 % int3))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Erin is not quiet.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule2)) -> rule5)) -> rule4) OR ((((triple2 ((triple2) -> rule2)) -> rule5) ((triple2) -> rule2)) -> rule8))]
("Erin" "is" "quiet" "-")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((triple2) -> (rule2 % int3))) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "nice" "-")
Harry is cold.
Unknown
rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Harry" "is" "cold" "+")
Harry is not quiet.
Unknown
inv-rconc
[@3: Harry is quiet.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule3 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is nice.
Unknown
rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "nice" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Bob is cold.[(triple1)] Erin is nice.[(triple2)] Gary is nice.[(triple3)] Harry is blue.[(triple4)] @1: Bob is furry.[(((triple1) -> rule7))] Bob is quiet.[(((triple1) -> rule4) OR ((triple1 ((triple1) -> rule7)) -> rule8))] Erin is furry.[(((triple2) -> rule2))] Gary is furry.[(((triple3) -> rule2))] Gary is smart.[(((triple3) -> rule6))] Harry is furry.[(((triple4) -> rule1))] @2: Erin is cold.[(((triple2 ((triple2) -> rule2)) -> rule5))] Gary is cold.[(((triple3 ((triple3) -> rule2)) -> rule5))] @3: Erin is quiet.[(((((triple2 ((triple2) -> rule2)) -> rule5)) -> rule4) OR ((((triple2 ((triple2) -> rule2)) -> rule5) ((triple2) -> rule2)) -> rule8))] Gary is quiet.[(((((triple3 ((triple3) -> rule2)) -> rule5)) -> rule4) OR ((((triple3 ((triple3) -> rule2)) -> rule5) ((triple3) -> rule2)) -> rule8))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple1 ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple3) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple3) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((triple2) -> (rule2 % int3))) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule5 % int2)) ((triple3) -> (rule2 % int3))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3