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