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