Bob is big. Bob is blue. Bob is furry. Erin is big. Erin is blue. Erin is cold. Erin is rough. Harry is not blue. Harry is furry. Harry is nice. Harry is rough. Harry is smart. If Harry is cold and Harry is big then Harry is blue. If Harry is rough and Harry is cold then Harry is big. Rough, smart people are furry. If someone is furry and not big then they are smart. If someone is rough and cold then they are smart. If someone is smart and not cold then they are blue. All furry people are nice. If someone is cold and furry then they are nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Harry is cold and Harry is big then Harry is blue.
((("Harry" "is" "cold" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "blue" "+"))
If Harry is rough and Harry is cold then Harry is big.
((("Harry" "is" "rough" "+") ("Harry" "is" "cold" "+")) -> ("Harry" "is" "big" "+"))
Rough, smart people are furry.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry and not big then they are smart.
((("someone" "is" "furry" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "smart" "+"))
If someone is rough and cold then they are smart.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and not cold then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "blue" "+"))
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold and furry then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
Harry is rough.
True
1
proof
[(triple11)]
("Harry" "is" "rough" "+")
triple11
Harry is not nice.
False
1
inv-proof
[(triple10 OR ((triple9) -> rule7) OR ((((triple11 triple12) -> rule3)) -> rule7))]
("Harry" "is" "nice" "-")
triple10
((triple9) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple11 triple12) -> (rule3 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Bob is nice.
True
2
proof
[(((triple3) -> rule7))]
("Bob" "is" "nice" "+")
((triple3) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Erin is not smart.
False
3
inv-proof
[(((triple7 triple6) -> rule5))]
("Erin" "is" "smart" "-")
((triple7 triple6) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
True
5
proof
[(((triple7 ((triple7 triple6) -> rule5)) -> rule3))]
("Erin" "is" "furry" "+")
((triple7 ((triple7 triple6) -> (rule5 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not furry.
False
5
inv-proof
[(((triple7 ((triple7 triple6) -> rule5)) -> rule3))]
("Erin" "is" "furry" "-")
((triple7 ((triple7 triple6) -> (rule5 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is nice.
True
6
proof
[(((((triple7 ((triple7 triple6) -> rule5)) -> rule3)) -> rule7) OR ((triple6 ((triple7 ((triple7 triple6) -> rule5)) -> rule3)) -> rule8))]
("Erin" "is" "nice" "+")
((((triple7 ((triple7 triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((triple6 ((triple7 ((triple7 triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not nice.
False
6
inv-proof
[(((((triple7 ((triple7 triple6) -> rule5)) -> rule3)) -> rule7) OR ((triple6 ((triple7 ((triple7 triple6) -> rule5)) -> rule3)) -> rule8))]
("Erin" "is" "nice" "-")
((((triple7 ((triple7 triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((triple6 ((triple7 ((triple7 triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "smart" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "big" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is furry.[(triple3)] Erin is big.[(triple4)] Erin is blue.[(triple5)] Erin is cold.[(triple6)] Erin is rough.[(triple7)] Harry is furry.[(triple9 OR ((triple11 triple12) -> rule3))] Harry is nice.[(triple10 OR ((triple9) -> rule7) OR ((((triple11 triple12) -> rule3)) -> rule7))] Harry is not blue.[(triple8)] Harry is rough.[(triple11)] Harry is smart.[(triple12)] @1: Bob is nice.[(((triple3) -> rule7))] Erin is smart.[(((triple7 triple6) -> rule5))] @2: Erin is furry.[(((triple7 ((triple7 triple6) -> rule5)) -> rule3))] @3: Erin is nice.[(((((triple7 ((triple7 triple6) -> rule5)) -> rule3)) -> rule7) OR ((triple6 ((triple7 ((triple7 triple6) -> rule5)) -> rule3)) -> rule8))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple9
((triple11 triple12) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple10
((triple9) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple11 triple12) -> (rule3 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not blue.
("Harry" "is" "blue" "-")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Bob is nice.
("Bob" "is" "nice" "+")
((triple3) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple7 triple6) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple7 ((triple7 triple6) -> (rule5 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple7 ((triple7 triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((triple6 ((triple7 ((triple7 triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3