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