Bob is cold. Bob is kind. Bob is nice. Dave is not blue. Dave is cold. Dave is green. Dave is kind. Dave is nice. Dave is smart. Fiona is kind. Fiona is not smart. Harry is blue. All kind, green things are smart. Blue, nice things are smart. If something is kind and nice then it is cold. All kind things are cold. All red, smart things are green. Smart things are not red. If Bob is nice and Bob is green then Bob is red. If Bob is red then Bob is not kind.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is not smart.
("Fiona" "is" "smart" "-")
Harry is blue.
("Harry" "is" "blue" "+")
All kind, green things are smart.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Blue, nice things are smart.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If something is kind and nice then it is cold.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
All kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
All red, smart things are green.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Smart things are not red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "-"))
If Bob is nice and Bob is green then Bob is red.
((("Bob" "is" "nice" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "red" "+"))
If Bob is red then Bob is not kind.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "kind" "-"))
Dave is cold.
True
1
proof
[(triple5 OR ((triple7) -> rule4) OR ((triple7 triple8) -> rule3))]
("Dave" "is" "cold" "+")
triple5
((triple7) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple7 triple8) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Bob is not nice.
False
1
inv-proof
[(triple3)]
("Bob" "is" "nice" "-")
triple3
Bob is not green.
Unknown
inv-rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("Bob" "is" "green" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Bob is cold.[(triple1 OR ((triple2) -> rule4) OR ((triple2 triple3) -> rule3))] Bob is kind.[(triple2)] Bob is nice.[(triple3)] Dave is cold.[(triple5 OR ((triple7) -> rule4) OR ((triple7 triple8) -> rule3))] Dave is green.[(triple6)] Dave is kind.[(triple7)] Dave is nice.[(triple8)] Dave is not blue.[(triple4)] Dave is smart.[(triple9 OR ((triple7 triple6) -> rule1))] Fiona is kind.[(triple10)] Fiona is not smart.[(triple11)] Harry is blue.[(triple12)] @1: Dave is not red.[(((triple9) -> rule6) OR ((((triple7 triple6) -> rule1)) -> rule6))] Fiona is cold.[(((triple10) -> rule4))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple2) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple2 triple3) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple5
((triple7) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple7 triple8) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
triple8
Dave is not blue.
("Dave" "is" "blue" "-")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple9
((triple7 triple6) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple10
Fiona is not smart.
("Fiona" "is" "smart" "-")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Dave is not red.
("Dave" "is" "red" "-")
((triple9) -> (rule6 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
((((triple7 triple6) -> (rule1 % int2))) -> (rule6 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple10) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1