Anne is kind. Charlie is young. Kind people are cold. If someone is young then they are cold. If someone is young then they are blue. Cold people are round. All round people are young. All round people are cold. All blue people are kind. If someone is blue and green then they are round.
Anne is kind.
("Anne" "is" "kind" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is young then they are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is young then they are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
All round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
All round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue and green then they are round.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is kind.[(triple1)] Charlie is young.[(triple2)] @1: Anne is cold.[(((triple1) -> rule1))] Charlie is blue.[(((triple2) -> rule3))] Charlie is cold.[(((triple2) -> rule2) OR ((((((triple2) -> rule3)) -> rule7)) -> rule1))] @2: Anne is round.[(((((triple1) -> rule1)) -> rule4))] Charlie is kind.[(((((triple2) -> rule3)) -> rule7))] Charlie is round.[(((((triple2) -> rule2)) -> rule4) OR ((((((((triple2) -> rule3)) -> rule7)) -> rule1)) -> rule4))] @3: Anne is young.[(((((((triple1) -> rule1)) -> rule4)) -> rule5))] @4: Anne is blue.[(((((((((triple1) -> rule1)) -> rule4)) -> rule5)) -> rule3))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((((((triple2) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4