Charlie is blue. Charlie is white. Harry is cold. All quiet people are cold. If someone is quiet then they are kind. Cold, quiet people are young. If Charlie is white then Charlie is blue. White people are big. Big people are quiet.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
All quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If someone is quiet then they are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Cold, quiet people are young.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If Charlie is white then Charlie is blue.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "blue" "+"))
White people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
Harry is cold.
True
1
proof
[(triple3)]
("Harry" "is" "cold" "+")
triple3
Harry is not cold.
False
1
inv-proof
[(triple3)]
("Harry" "is" "cold" "-")
triple3
Charlie is big.
True
2
proof
[(((triple2) -> rule5))]
("Charlie" "is" "big" "+")
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "big" "-")
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
True
3
proof
[(((((triple2) -> rule5)) -> rule6))]
("Charlie" "is" "quiet" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not quiet.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule6))]
("Charlie" "is" "quiet" "-")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is cold.
True
4
proof
[(((((((triple2) -> rule5)) -> rule6)) -> rule1))]
("Charlie" "is" "cold" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not kind.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule6)) -> rule2))]
("Charlie" "is" "kind" "-")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Harry is not quiet.
Unknown
inv-rconc
[@2: Harry is quiet.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "big" "+")
Harry is not kind.
Unknown
inv-rconc
[@3: Harry is kind.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule5 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is young.
Unknown
rconc
[@3: Harry is young.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule5 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Charlie is blue.[(triple1 OR ((triple2) -> rule4))] Charlie is white.[(triple2)] Harry is cold.[(triple3)] @1: Charlie is big.[(((triple2) -> rule5))] @2: Charlie is quiet.[(((((triple2) -> rule5)) -> rule6))] @3: Charlie is cold.[(((((((triple2) -> rule5)) -> rule6)) -> rule1))] Charlie is kind.[(((((((triple2) -> rule5)) -> rule6)) -> rule2))] @4: Charlie is young.[(((((((((triple2) -> rule5)) -> rule6)) -> rule1) ((((triple2) -> rule5)) -> rule6)) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple2) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Harry is cold.
("Harry" "is" "cold" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
((((((((triple2) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((((triple2) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4