Bob is furry. Bob is nice. Bob is rough. Erin is blue. Erin is smart. Erin is white. Gary is cold. If something is cold then it is rough. If Bob is not nice then Bob is cold. All blue things are white. If Gary is smart and Gary is not cold then Gary is furry. If something is furry and not cold then it is blue. All rough, furry things are blue. Blue, white things are smart. If Gary is smart then Gary is rough.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If something is cold then it is rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If Bob is not nice then Bob is cold.
((("Bob" "is" "nice" "~")) -> ("Bob" "is" "cold" "+"))
All blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If Gary is smart and Gary is not cold then Gary is furry.
((("Gary" "is" "smart" "+") ("Gary" "is" "cold" "~")) -> ("Gary" "is" "furry" "+"))
If something is furry and not cold then it is blue.
((("something" "is" "furry" "+") ("something" "is" "cold" "~")) -> ("something" "is" "blue" "+"))
All rough, furry things are blue.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Blue, white things are smart.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If Gary is smart then Gary is rough.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "rough" "+"))
Erin is smart.
True
1
proof
[(triple5 OR ((triple4 triple6) -> rule7) OR ((triple4 ((triple4) -> rule3)) -> rule7))]
("Erin" "is" "smart" "+")
triple5
((triple4 triple6) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple4 ((triple4) -> (rule3 % int2))) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Bob is not nice.
False
1
inv-proof
[(triple2)]
("Bob" "is" "nice" "-")
triple2
Gary is rough.
True
2
proof
[(((triple7) -> rule1))]
("Gary" "is" "rough" "+")
((triple7) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Bob is not blue.
False
3
inv-proof
[(((triple3 triple1) -> rule6))]
("Bob" "is" "blue" "-")
((triple3 triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
True
4
proof
[(((((triple3 triple1) -> rule6)) -> rule3))]
("Bob" "is" "white" "+")
((((triple3 triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not white.
False
4
inv-proof
[(((((triple3 triple1) -> rule6)) -> rule3))]
("Bob" "is" "white" "-")
((((triple3 triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
True
8
proof
[(((((triple3 triple1) -> rule6) ((((triple3 triple1) -> rule6)) -> rule3)) -> rule7))]
("Bob" "is" "smart" "+")
((((triple3 triple1) -> (rule6 % int3)) ((((triple3 triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not smart.
False
8
inv-proof
[(((((triple3 triple1) -> rule6) ((((triple3 triple1) -> rule6)) -> rule3)) -> rule7))]
("Bob" "is" "smart" "-")
((((triple3 triple1) -> (rule6 % int3)) ((((triple3 triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Gary is not smart.
Unknown
inv-rconc
[@3: Gary is smart.[CWA. Example of deepest failure = (rule7 <- rule6 <- rule4 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is blue.
Unknown
rconc
[@2: Gary is blue.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Gary" "is" "blue" "+")
Gary is not white.
Unknown
inv-rconc
[@3: Gary is white.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule4 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "furry" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Bob is furry.[(triple1)] Bob is nice.[(triple2)] Bob is rough.[(triple3)] Erin is blue.[(triple4)] Erin is smart.[(triple5 OR ((triple4 triple6) -> rule7) OR ((triple4 ((triple4) -> rule3)) -> rule7))] Erin is white.[(triple6 OR ((triple4) -> rule3))] Gary is cold.[(triple7)] @1: Bob is blue.[(((triple3 triple1) -> rule6))] Gary is rough.[(((triple7) -> rule1))] @2: Bob is white.[(((((triple3 triple1) -> rule6)) -> rule3))] @3: Bob is smart.[(((((triple3 triple1) -> rule6) ((((triple3 triple1) -> rule6)) -> rule3)) -> rule7))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Erin is smart.
("Erin" "is" "smart" "+")
triple5
((triple4 triple6) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple4 ((triple4) -> (rule3 % int2))) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple6
((triple4) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Bob is blue.
("Bob" "is" "blue" "+")
((triple3 triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple7) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple3 triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((triple3 triple1) -> (rule6 % int3)) ((((triple3 triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3