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