Bob is not cold. Bob is not nice. Bob is quiet. Bob is smart. Erin is blue. Erin is not smart. Gary is big. Gary is blue. Gary is furry. Gary is nice. Gary is quiet. Gary is smart. Big things are furry. If something is blue and quiet then it is big. If Gary is quiet then Gary is smart. If Bob is quiet then Bob is blue. If Bob is furry and Bob is big then Bob is smart. If Bob is quiet and Bob is not big then Bob is not furry. If something is furry and not smart then it is nice. If something is quiet and not big then it is nice.
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Big things are furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If something is blue and quiet then it is big.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If Gary is quiet then Gary is smart.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "smart" "+"))
If Bob is quiet then Bob is blue.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "blue" "+"))
If Bob is furry and Bob is big then Bob is smart.
((("Bob" "is" "furry" "+") ("Bob" "is" "big" "+")) -> ("Bob" "is" "smart" "+"))
If Bob is quiet and Bob is not big then Bob is not furry.
((("Bob" "is" "quiet" "+") ("Bob" "is" "big" "~")) -> ("Bob" "is" "furry" "-"))
If something is furry and not smart then it is nice.
((("something" "is" "furry" "+") ("something" "is" "smart" "~")) -> ("something" "is" "nice" "+"))
If something is quiet and not big then it is nice.
((("something" "is" "quiet" "+") ("something" "is" "big" "~")) -> ("something" "is" "nice" "+"))
Gary is furry.
True
1
proof
[(triple9 OR ((triple7) -> rule1) OR ((((triple8 triple11) -> rule2)) -> rule1))]
("Gary" "is" "furry" "+")
triple9
((triple7) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple8 triple11) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Erin is smart.
False
1
inv-proof
[(triple6)]
("Erin" "is" "smart" "+")
triple6
Bob is blue.
True
2
proof
[(((triple3) -> rule4))]
("Bob" "is" "blue" "+")
((triple3) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple3) -> rule4))]
("Bob" "is" "blue" "-")
((triple3) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
True
4
proof
[(((((triple3) -> rule4) triple3) -> rule2))]
("Bob" "is" "big" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not big.
False
4
inv-proof
[(((((triple3) -> rule4) triple3) -> rule2))]
("Bob" "is" "big" "-")
((((triple3) -> (rule4 % int2)) triple3) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is furry.
True
5
proof
[(((((((triple3) -> rule4) triple3) -> rule2)) -> rule1))]
("Bob" "is" "furry" "+")
((((((triple3) -> (rule4 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not furry.
False
5
inv-proof
[(((((((triple3) -> rule4) triple3) -> rule2)) -> rule1))]
("Bob" "is" "furry" "-")
((((((triple3) -> (rule4 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "big" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "nice" "+")
Erin is not furry.
Unknown
inv-rconc
[@2: Erin is furry.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Erin" "is" "furry" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Bob is not cold.[(triple1)] Bob is not nice.[(triple2)] Bob is quiet.[(triple3)] Bob is smart.[(triple4 OR ((((((((triple3) -> rule4) triple3) -> rule2)) -> rule1) ((((triple3) -> rule4) triple3) -> rule2)) -> rule5))] Erin is blue.[(triple5)] Erin is not smart.[(triple6)] Gary is big.[(triple7 OR ((triple8 triple11) -> rule2))] Gary is blue.[(triple8)] Gary is furry.[(triple9 OR ((triple7) -> rule1) OR ((((triple8 triple11) -> rule2)) -> rule1))] Gary is nice.[(triple10)] Gary is quiet.[(triple11)] Gary is smart.[(triple12 OR ((triple11) -> rule3))] @1: Bob is blue.[(((triple3) -> rule4))] @2: Bob is big.[(((((triple3) -> rule4) triple3) -> rule2))] @3: Bob is furry.[(((((((triple3) -> rule4) triple3) -> rule2)) -> rule1))]
Bob is not cold.
("Bob" "is" "cold" "-")
triple1
Bob is not nice.
("Bob" "is" "nice" "-")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
((((((((triple3) -> (rule4 % int4)) triple3) -> (rule2 % int3))) -> (rule1 % int2)) ((((triple3) -> (rule4 % int4)) triple3) -> (rule2 % int3))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is not smart.
("Erin" "is" "smart" "-")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
((triple8 triple11) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Gary is furry.
("Gary" "is" "furry" "+")
triple9
((triple7) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple8 triple11) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
triple12
((triple11) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple3) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple3) -> (rule4 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3