Anne is kind. Erin is kind. Kind things are smart. White, big things are blue. If something is red then it is big. All kind things are big. If something is white and big then it is blue. Green things are red. Kind, smart things are green. All blue, smart things are red.
Anne is kind.
("Anne" "is" "kind" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
White, big things are blue.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is red then it is big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
All kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If something is white and big then it is blue.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
Green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Kind, smart things are green.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All blue, smart things are red.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Erin is kind.
True
1
proof
[(triple2)]
("Erin" "is" "kind" "+")
triple2
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Erin is smart.
True
2
proof
[(((triple2) -> rule1))]
("Erin" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule4) OR ((((((triple1 ((triple1) -> rule1)) -> rule7)) -> rule6)) -> rule3))]
("Anne" "is" "big" "-")
((triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((((triple1 ((triple1) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Erin is green.
True
4
proof
[(((triple2 ((triple2) -> rule1)) -> rule7))]
("Erin" "is" "green" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not green.
False
4
inv-proof
[(((triple2 ((triple2) -> rule1)) -> rule7))]
("Erin" "is" "green" "-")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is red.
True
5
proof
[(((((triple2 ((triple2) -> rule1)) -> rule7)) -> rule6))]
("Erin" "is" "red" "+")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not red.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule1)) -> rule7)) -> rule6))]
("Erin" "is" "red" "-")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "blue" "-")
Anne is blue.
Unknown
rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "blue" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Anne is kind.[(triple1)] Erin is kind.[(triple2)] @1: Anne is big.[(((triple1) -> rule4) OR ((((((triple1 ((triple1) -> rule1)) -> rule7)) -> rule6)) -> rule3))] Anne is smart.[(((triple1) -> rule1))] Erin is big.[(((triple2) -> rule4) OR ((((((triple2 ((triple2) -> rule1)) -> rule7)) -> rule6)) -> rule3))] Erin is smart.[(((triple2) -> rule1))] @2: Anne is green.[(((triple1 ((triple1) -> rule1)) -> rule7))] Erin is green.[(((triple2 ((triple2) -> rule1)) -> rule7))] @3: Anne is red.[(((((triple1 ((triple1) -> rule1)) -> rule7)) -> rule6))] Erin is red.[(((((triple2 ((triple2) -> rule1)) -> rule7)) -> rule6))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((((triple1 ((triple1) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple2) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((((triple2 ((triple2) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3