Bob is blue. Bob is cold. Bob is furry. Bob is red. Dave is cold. Dave is kind. Dave is smart. Erin is big. Erin is not blue. Erin is kind. Erin is red. Erin is smart. Harry is blue. Harry is red. Harry is smart. If something is blue then it is big. Red, blue things are big. All big, furry things are smart. If Erin is smart then Erin is furry. Blue, smart things are not kind. If something is red and not smart then it is not kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Red, blue things are big.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
All big, furry things are smart.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If Erin is smart then Erin is furry.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "furry" "+"))
Blue, smart things are not kind.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "-"))
If something is red and not smart then it is not kind.
((("something" "is" "red" "+") ("something" "is" "smart" "~")) -> ("something" "is" "kind" "-"))
Harry is blue.
True
1
proof
[(triple13)]
("Harry" "is" "blue" "+")
triple13
Bob is not red.
False
1
inv-proof
[(triple4)]
("Bob" "is" "red" "-")
triple4
Harry is big.
True
2
proof
[(((triple13) -> rule1) OR ((triple14 triple13) -> rule2))]
("Harry" "is" "big" "+")
((triple13) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple14 triple13) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
False
3
inv-proof
[(((triple13 triple15) -> rule5))]
("Harry" "is" "kind" "+")
((triple13 triple15) -> (rule5 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Bob is smart.
True
4
proof
[(((((triple1) -> rule1) triple3) -> rule3) OR ((((triple4 triple1) -> rule2) triple3) -> rule3))]
("Bob" "is" "smart" "+")
((((triple1) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple4 triple1) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not smart.
False
4
inv-proof
[(((((triple1) -> rule1) triple3) -> rule3) OR ((((triple4 triple1) -> rule2) triple3) -> rule3))]
("Bob" "is" "smart" "-")
((((triple1) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple4 triple1) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not kind.
True
6
proof
[(((triple1 ((((triple1) -> rule1) triple3) -> rule3)) -> rule5) OR ((triple1 ((((triple4 triple1) -> rule2) triple3) -> rule3)) -> rule5))]
("Bob" "is" "kind" "-")
((triple1 ((((triple1) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule5 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((triple1 ((((triple4 triple1) -> (rule2 % int3)) triple3) -> (rule3 % int2))) -> (rule5 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is kind.
False
6
inv-proof
[(((triple1 ((((triple1) -> rule1) triple3) -> rule3)) -> rule5) OR ((triple1 ((((triple4 triple1) -> rule2) triple3) -> rule3)) -> rule5))]
("Bob" "is" "kind" "+")
((triple1 ((((triple1) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule5 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((triple1 ((((triple4 triple1) -> (rule2 % int3)) triple3) -> (rule3 % int2))) -> (rule5 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is furry.[(triple3)] Bob is red.[(triple4)] Dave is cold.[(triple5)] Dave is kind.[(triple6)] Dave is smart.[(triple7)] Erin is big.[(triple8)] Erin is kind.[(triple10)] Erin is not blue.[(triple9)] Erin is red.[(triple11)] Erin is smart.[(triple12)] Harry is blue.[(triple13)] Harry is red.[(triple14)] Harry is smart.[(triple15)] @1: Bob is big.[(((triple1) -> rule1) OR ((triple4 triple1) -> rule2))] Erin is furry.[(((triple12) -> rule4))] Harry is big.[(((triple13) -> rule1) OR ((triple14 triple13) -> rule2))] Harry is not kind.[(((triple13 triple15) -> rule5))] @2: Bob is smart.[(((((triple1) -> rule1) triple3) -> rule3) OR ((((triple4 triple1) -> rule2) triple3) -> rule3))] @3: Bob is not kind.[(((triple1 ((((triple1) -> rule1) triple3) -> rule3)) -> rule5) OR ((triple1 ((((triple4 triple1) -> rule2) triple3) -> rule3)) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is kind.
("Erin" "is" "kind" "+")
triple10
Erin is not blue.
("Erin" "is" "blue" "-")
triple9
Erin is red.
("Erin" "is" "red" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Harry is blue.
("Harry" "is" "blue" "+")
triple13
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple4 triple1) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple12) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple13) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple14 triple13) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not kind.
("Harry" "is" "kind" "-")
((triple13 triple15) -> (rule5 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple4 triple1) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not kind.
("Bob" "is" "kind" "-")
((triple1 ((((triple1) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule5 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((triple1 ((((triple4 triple1) -> (rule2 % int3)) triple3) -> (rule3 % int2))) -> (rule5 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3