Bob is cold. Dave is nice. Harry is young. If Bob is rough and Bob is blue then Bob is nice. If someone is young then they are green. All young, rough people are nice. If someone is blue and not red then they are young. If someone is red then they are cold. If someone is green and young then they are blue.
Bob is cold.
("Bob" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Harry is young.
("Harry" "is" "young" "+")
If Bob is rough and Bob is blue then Bob is nice.
((("Bob" "is" "rough" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "nice" "+"))
If someone is young then they are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
All young, rough people are nice.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is blue and not red then they are young.
((("someone" "is" "blue" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "young" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is green and young then they are blue.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Bob is cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Dave is not nice.
False
1
inv-proof
[(triple2)]
("Dave" "is" "nice" "-")
triple2
Harry is green.
True
2
proof
[(((triple3) -> rule2))]
("Harry" "is" "green" "+")
((triple3) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple3) -> rule2))]
("Harry" "is" "green" "-")
((triple3) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
True
4
proof
[(((((triple3) -> rule2) triple3) -> rule6))]
("Harry" "is" "blue" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not blue.
False
4
inv-proof
[(((((triple3) -> rule2) triple3) -> rule6))]
("Harry" "is" "blue" "-")
((((triple3) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Bob is not green.
Unknown
inv-rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Bob" "is" "green" "-")
Dave is blue.
Unknown
rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Dave" "is" "blue" "+")
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "nice" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Bob is cold.[(triple1)] Dave is nice.[(triple2)] Harry is young.[(triple3)] @1: Harry is green.[(((triple3) -> rule2))] @2: Harry is blue.[(((((triple3) -> rule2) triple3) -> rule6))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
((triple3) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2