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