Anne is young. Dave is blue. Dave is kind. Erin is smart. Erin is white. Erin is young. Fiona is smart. Kind, green things are blue. Smart things are young. Nice, young things are blue. All blue things are white. All young, smart things are green. If something is white then it is blue. If something is green then it is kind. Nice things are young.
Anne is young.
("Anne" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Kind, green things are blue.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Nice, young things are blue.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
All young, smart things are green.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is white then it is blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If something is green then it is kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
Nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Erin is smart.
True
1
proof
[(triple4)]
("Erin" "is" "smart" "+")
triple4
Dave is not kind.
False
1
inv-proof
[(triple3)]
("Dave" "is" "kind" "-")
triple3
Erin is blue.
True
2
proof
[(((triple5) -> rule6) OR ((((((triple6 triple4) -> rule5)) -> rule7) ((triple6 triple4) -> rule5)) -> rule1) OR ((((((triple6 triple4) -> rule5)) -> rule7) ((((triple4) -> rule2) triple4) -> rule5)) -> rule1) OR ((((((((triple4) -> rule2) triple4) -> rule5)) -> rule7) ((triple6 triple4) -> rule5)) -> rule1) OR ((((((((triple4) -> rule2) triple4) -> rule5)) -> rule7) ((((triple4) -> rule2) triple4) -> rule5)) -> rule1))]
("Erin" "is" "blue" "+")
((triple5) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((((triple6 triple4) -> (rule5 % int3))) -> (rule7 % int2)) ((triple6 triple4) -> (rule5 % int3))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((triple6 triple4) -> (rule5 % int4))) -> (rule7 % int3)) ((((triple4) -> (rule2 % int2)) triple4) -> (rule5 % int4))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
((((((((triple4) -> (rule2 % int4)) triple4) -> (rule5 % int3))) -> (rule7 % int2)) ((triple6 triple4) -> (rule5 % int3))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
((((((((triple4) -> (rule2 % int4)) triple4) -> (rule5 % int3))) -> (rule7 % int2)) ((((triple4) -> (rule2 % int4)) triple4) -> (rule5 % int3))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Fiona is not young.
False
2
inv-proof
[(((triple7) -> rule2))]
("Fiona" "is" "young" "-")
((triple7) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Erin is kind.
True
4
proof
[(((((triple6 triple4) -> rule5)) -> rule7) OR ((((((triple4) -> rule2) triple4) -> rule5)) -> rule7))]
("Erin" "is" "kind" "+")
((((triple6 triple4) -> (rule5 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((((triple4) -> (rule2 % int3)) triple4) -> (rule5 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not kind.
False
4
inv-proof
[(((((triple6 triple4) -> rule5)) -> rule7) OR ((((((triple4) -> rule2) triple4) -> rule5)) -> rule7))]
("Erin" "is" "kind" "-")
((((triple6 triple4) -> (rule5 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((((triple4) -> (rule2 % int3)) triple4) -> (rule5 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Fiona is kind.
True
5
proof
[(((((((triple7) -> rule2) triple7) -> rule5)) -> rule7))]
("Fiona" "is" "kind" "+")
((((((triple7) -> (rule2 % int3)) triple7) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is not kind.
False
5
inv-proof
[(((((((triple7) -> rule2) triple7) -> rule5)) -> rule7))]
("Fiona" "is" "kind" "-")
((((((triple7) -> (rule2 % int3)) triple7) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is blue.
True
10
proof
[(((((((((triple7) -> rule2) triple7) -> rule5)) -> rule7) ((((triple7) -> rule2) triple7) -> rule5)) -> rule1))]
("Fiona" "is" "blue" "+")
((((((((triple7) -> (rule2 % int4)) triple7) -> (rule5 % int3))) -> (rule7 % int2)) ((((triple7) -> (rule2 % int4)) triple7) -> (rule5 % int3))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Fiona is not blue.
False
10
inv-proof
[(((((((((triple7) -> rule2) triple7) -> rule5)) -> rule7) ((((triple7) -> rule2) triple7) -> rule5)) -> rule1))]
("Fiona" "is" "blue" "-")
((((((((triple7) -> (rule2 % int4)) triple7) -> (rule5 % int3))) -> (rule7 % int2)) ((((triple7) -> (rule2 % int4)) triple7) -> (rule5 % int3))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Fiona is white.
True
11
proof
[(((((((((((triple7) -> rule2) triple7) -> rule5)) -> rule7) ((((triple7) -> rule2) triple7) -> rule5)) -> rule1)) -> rule4))]
("Fiona" "is" "white" "+")
((((((((((triple7) -> (rule2 % int5)) triple7) -> (rule5 % int4))) -> (rule7 % int3)) ((((triple7) -> (rule2 % int5)) triple7) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
int5
Fiona is not white.
False
11
inv-proof
[(((((((((((triple7) -> rule2) triple7) -> rule5)) -> rule7) ((((triple7) -> rule2) triple7) -> rule5)) -> rule1)) -> rule4))]
("Fiona" "is" "white" "-")
((((((((((triple7) -> (rule2 % int5)) triple7) -> (rule5 % int4))) -> (rule7 % int3)) ((((triple7) -> (rule2 % int5)) triple7) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
int5
Anne is not white.
Unknown
inv-rconc
[@3: Anne is white.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule5 <- FAIL)]]
("Anne" "is" "white" "-")
Dave is young.
Unknown
rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "young" "+")
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is kind.
Unknown
rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("Anne" "is" "kind" "+")
Anne is not blue.
Unknown
inv-rconc
[@4: Anne is blue.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule1 <- rule5 <- FAIL)]]
("Anne" "is" "blue" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "green" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Anne is young.[(triple1)] Dave is blue.[(triple2)] Dave is kind.[(triple3)] Erin is smart.[(triple4)] Erin is white.[(triple5 OR ((((((((triple6 triple4) -> rule5)) -> rule7) ((triple6 triple4) -> rule5)) -> rule1)) -> rule4) OR ((((((((triple6 triple4) -> rule5)) -> rule7) ((((triple4) -> rule2) triple4) -> rule5)) -> rule1)) -> rule4) OR ((((((((((triple4) -> rule2) triple4) -> rule5)) -> rule7) ((triple6 triple4) -> rule5)) -> rule1)) -> rule4) OR ((((((((((triple4) -> rule2) triple4) -> rule5)) -> rule7) ((((triple4) -> rule2) triple4) -> rule5)) -> rule1)) -> rule4))] Erin is young.[(triple6 OR ((triple4) -> rule2))] Fiona is smart.[(triple7)] @1: Dave is white.[(((triple2) -> rule4))] Erin is blue.[(((triple5) -> rule6) OR ((((((triple6 triple4) -> rule5)) -> rule7) ((triple6 triple4) -> rule5)) -> rule1) OR ((((((triple6 triple4) -> rule5)) -> rule7) ((((triple4) -> rule2) triple4) -> rule5)) -> rule1) OR ((((((((triple4) -> rule2) triple4) -> rule5)) -> rule7) ((triple6 triple4) -> rule5)) -> rule1) OR ((((((((triple4) -> rule2) triple4) -> rule5)) -> rule7) ((((triple4) -> rule2) triple4) -> rule5)) -> rule1))] Erin is green.[(((triple6 triple4) -> rule5) OR ((((triple4) -> rule2) triple4) -> rule5))] Fiona is young.[(((triple7) -> rule2))] @2: Erin is kind.[(((((triple6 triple4) -> rule5)) -> rule7) OR ((((((triple4) -> rule2) triple4) -> rule5)) -> rule7))] Fiona is green.[(((((triple7) -> rule2) triple7) -> rule5))] @3: Fiona is kind.[(((((((triple7) -> rule2) triple7) -> rule5)) -> rule7))] @4: Fiona is blue.[(((((((((triple7) -> rule2) triple7) -> rule5)) -> rule7) ((((triple7) -> rule2) triple7) -> rule5)) -> rule1))] @5: Fiona is white.[(((((((((((triple7) -> rule2) triple7) -> rule5)) -> rule7) ((((triple7) -> rule2) triple7) -> rule5)) -> rule1)) -> rule4))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Erin is white.
("Erin" "is" "white" "+")
triple5
((((((((triple6 triple4) -> (rule5 % int4))) -> (rule7 % int3)) ((triple6 triple4) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
((((((((triple6 triple4) -> (rule5 % int5))) -> (rule7 % int4)) ((((triple4) -> (rule2 % int3)) triple4) -> (rule5 % int5))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5
((((((((((triple4) -> (rule2 % int5)) triple4) -> (rule5 % int4))) -> (rule7 % int3)) ((triple6 triple4) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
int5
((((((((((triple4) -> (rule2 % int5)) triple4) -> (rule5 % int4))) -> (rule7 % int3)) ((((triple4) -> (rule2 % int5)) triple4) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
int5
Erin is young.
("Erin" "is" "young" "+")
triple6
((triple4) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
((triple2) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple5) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((((triple6 triple4) -> (rule5 % int3))) -> (rule7 % int2)) ((triple6 triple4) -> (rule5 % int3))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((triple6 triple4) -> (rule5 % int4))) -> (rule7 % int3)) ((((triple4) -> (rule2 % int2)) triple4) -> (rule5 % int4))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
((((((((triple4) -> (rule2 % int4)) triple4) -> (rule5 % int3))) -> (rule7 % int2)) ((triple6 triple4) -> (rule5 % int3))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
((((((((triple4) -> (rule2 % int4)) triple4) -> (rule5 % int3))) -> (rule7 % int2)) ((((triple4) -> (rule2 % int4)) triple4) -> (rule5 % int3))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
((triple6 triple4) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple4) -> (rule2 % int2)) triple4) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((triple7) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple6 triple4) -> (rule5 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((((triple4) -> (rule2 % int3)) triple4) -> (rule5 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
((((triple7) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
((((((triple7) -> (rule2 % int3)) triple7) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
((((((((triple7) -> (rule2 % int4)) triple7) -> (rule5 % int3))) -> (rule7 % int2)) ((((triple7) -> (rule2 % int4)) triple7) -> (rule5 % int3))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
((((((((((triple7) -> (rule2 % int5)) triple7) -> (rule5 % int4))) -> (rule7 % int3)) ((((triple7) -> (rule2 % int5)) triple7) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
int5