Bob is green. Dave is rough. Harry is big. Kind, cold people are quiet. All quiet people are nice. If someone is rough then they are cold. If someone is kind then they are big. All big people are kind. If Dave is cold then Dave is kind. All nice, rough people are green. All nice, kind people are rough.
Bob is green.
("Bob" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Kind, cold people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
All big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If Dave is cold then Dave is kind.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "kind" "+"))
All nice, rough people are green.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
All nice, kind people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Harry is not big.
False
1
inv-proof
[(triple3)]
("Harry" "is" "big" "-")
triple3
Dave is cold.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "cold" "+")
((triple2) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple3) -> rule5))]
("Harry" "is" "kind" "-")
((triple3) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Dave is kind.
True
3
proof
[(((((triple2) -> rule3)) -> rule6))]
("Dave" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule6))]
("Dave" "is" "kind" "-")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Bob is not cold.
Unknown
inv-rconc
[@4: Bob is cold.[CWA. Example of deepest failure = (rule3 <- rule8 <- rule2 <- rule1 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is nice.
Unknown
rconc
[@4: Bob is nice.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule5 <- rule4 <- FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is green.[(triple1)] Dave is rough.[(triple2)] Harry is big.[(triple3)] @1: Dave is cold.[(((triple2) -> rule3))] Harry is kind.[(((triple3) -> rule5))] @2: Dave is kind.[(((((triple2) -> rule3)) -> rule6))] @3: Dave is big.[(((((((triple2) -> rule3)) -> rule6)) -> rule4))] Dave is quiet.[(((((((triple2) -> rule3)) -> rule6) ((triple2) -> rule3)) -> rule1))] @4: Dave is nice.[(((((((((triple2) -> rule3)) -> rule6) ((triple2) -> rule3)) -> rule1)) -> rule2))] @5: Dave is green.[(((((((((((triple2) -> rule3)) -> rule6) ((triple2) -> rule3)) -> rule1)) -> rule2) triple2) -> rule7))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
((triple2) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple3) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2)) ((triple2) -> (rule3 % int3))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((((((triple2) -> (rule3 % int4))) -> (rule6 % int3)) ((triple2) -> (rule3 % int4))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
((((((((((triple2) -> (rule3 % int5))) -> (rule6 % int4)) ((triple2) -> (rule3 % int5))) -> (rule1 % int3))) -> (rule2 % int2)) triple2) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
int5