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