Bob is nice. Harry is young. All nice, big people are young. All kind, nice people are cold. All young, big people are nice. Red people are cold. If someone is young then they are big. All nice, young people are kind.
Bob is nice.
("Bob" "is" "nice" "+")
Harry is young.
("Harry" "is" "young" "+")
All nice, big people are young.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
All kind, nice people are cold.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
All young, big people are nice.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is young then they are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
All nice, young people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Bob is not nice.
False
1
inv-proof
[(triple1)]
("Bob" "is" "nice" "-")
triple1
Harry is big.
True
2
proof
[(((triple2) -> rule5))]
("Harry" "is" "big" "+")
((triple2) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple2) -> rule5))]
("Harry" "is" "big" "-")
((triple2) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
True
4
proof
[(((triple2 ((triple2) -> rule5)) -> rule3))]
("Harry" "is" "nice" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not nice.
False
4
inv-proof
[(((triple2 ((triple2) -> rule5)) -> rule3))]
("Harry" "is" "nice" "-")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is kind.
True
6
proof
[(((((triple2 ((triple2) -> rule5)) -> rule3) triple2) -> rule6))]
("Harry" "is" "kind" "+")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule3 % int2)) triple2) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not kind.
False
6
inv-proof
[(((((triple2 ((triple2) -> rule5)) -> rule3) triple2) -> rule6))]
("Harry" "is" "kind" "-")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule3 % int2)) triple2) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Bob is not young.
Unknown
inv-rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Bob" "is" "young" "-")
Bob is cold.
Unknown
rconc
[@4: Bob is cold.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule1 <- rule5 <- FAIL)]]
("Bob" "is" "cold" "+")
Bob is not big.
Unknown
inv-rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is kind.
Unknown
rconc
[@3: Bob is kind.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule5 <- FAIL)]]
("Bob" "is" "kind" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Bob is nice.[(triple1)] Harry is young.[(triple2)] @1: Harry is big.[(((triple2) -> rule5))] @2: Harry is nice.[(((triple2 ((triple2) -> rule5)) -> rule3))] @3: Harry is kind.[(((((triple2 ((triple2) -> rule5)) -> rule3) triple2) -> rule6))] @4: Harry is cold.[(((((((triple2 ((triple2) -> rule5)) -> rule3) triple2) -> rule6) ((triple2 ((triple2) -> rule5)) -> rule3)) -> rule2))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Harry is young.
("Harry" "is" "young" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
((triple2) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule3 % int2)) triple2) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple2 ((triple2) -> (rule5 % int4))) -> (rule3 % int3)) triple2) -> (rule6 % int2)) ((triple2 ((triple2) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4