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