Bob is big. Bob is cold. Bob is furry. Bob is nice. Bob is quiet. Bob is red. Dave is big. Dave is furry. Dave is nice. Dave is quiet. Dave is red. Dave is smart. Erin is red. Harry is big. Harry is furry. Harry is quiet. If Erin is big and Erin is furry then Erin is cold. If Bob is nice and Bob is not big then Bob is quiet. If someone is red then they are cold. If someone is furry then they are nice. Cold, big people are smart. If someone is big and not furry then they are red. Smart people are quiet. If someone is big and not red then they are quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Erin is big and Erin is furry then Erin is cold.
((("Erin" "is" "big" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "cold" "+"))
If Bob is nice and Bob is not big then Bob is quiet.
((("Bob" "is" "nice" "+") ("Bob" "is" "big" "~")) -> ("Bob" "is" "quiet" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is furry then they are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
Cold, big people are smart.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If someone is big and not furry then they are red.
((("someone" "is" "big" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "red" "+"))
Smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If someone is big and not red then they are quiet.
((("someone" "is" "big" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "quiet" "+"))
Bob is nice.
True
1
proof
[(triple4 OR ((triple3) -> rule4))]
("Bob" "is" "nice" "+")
triple4
((triple3) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Dave is not nice.
False
1
inv-proof
[(triple9 OR ((triple8) -> rule4))]
("Dave" "is" "nice" "-")
triple9
((triple8) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Erin is not quiet.
Unknown
inv-rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2 OR ((triple6) -> rule3))] Bob is furry.[(triple3)] Bob is nice.[(triple4 OR ((triple3) -> rule4))] Bob is quiet.[(triple5 OR ((((triple2 triple1) -> rule5)) -> rule7) OR ((((((triple6) -> rule3) triple1) -> rule5)) -> rule7))] Bob is red.[(triple6)] Dave is big.[(triple7)] Dave is furry.[(triple8)] Dave is nice.[(triple9 OR ((triple8) -> rule4))] Dave is quiet.[(triple10 OR ((triple12) -> rule7) OR ((((((triple11) -> rule3) triple7) -> rule5)) -> rule7))] Dave is red.[(triple11)] Dave is smart.[(triple12 OR ((((triple11) -> rule3) triple7) -> rule5))] Erin is red.[(triple13)] Harry is big.[(triple14)] Harry is furry.[(triple15)] Harry is quiet.[(triple16)] @1: Bob is smart.[(((triple2 triple1) -> rule5) OR ((((triple6) -> rule3) triple1) -> rule5))] Dave is cold.[(((triple11) -> rule3))] Erin is cold.[(((triple13) -> rule3))] Harry is nice.[(((triple15) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple6) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((triple3) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((((triple2 triple1) -> (rule5 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((((triple6) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
triple6
Dave is big.
("Dave" "is" "big" "+")
triple7
Dave is furry.
("Dave" "is" "furry" "+")
triple8
Dave is nice.
("Dave" "is" "nice" "+")
triple9
((triple8) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10
((triple12) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((((triple11) -> (rule3 % int3)) triple7) -> (rule5 % int2))) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
triple11
Dave is smart.
("Dave" "is" "smart" "+")
triple12
((((triple11) -> (rule3 % int2)) triple7) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple13
Harry is big.
("Harry" "is" "big" "+")
triple14
Harry is furry.
("Harry" "is" "furry" "+")
triple15
Harry is quiet.
("Harry" "is" "quiet" "+")
triple16
Bob is smart.
("Bob" "is" "smart" "+")
((triple2 triple1) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple6) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((triple11) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple13) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple15) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1