Erin is cold. Erin is green. Erin is white. Fiona is cold. Fiona is green. Harry is green. Harry is quiet. If something is kind and young then it is round. All green, round things are quiet. All white things are quiet. All cold things are white. Quiet things are green. If something is kind and white then it is cold. All green, quiet things are round. Quiet, young things are green.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is kind and young then it is round.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
All green, round things are quiet.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
All white things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
All cold things are white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is kind and white then it is cold.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
All green, quiet things are round.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
Quiet, young things are green.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Harry is green.
True
1
proof
[(triple6 OR ((triple7) -> rule5))]
("Harry" "is" "green" "+")
triple6
((triple7) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Erin is not green.
False
1
inv-proof
[(triple2 OR ((((triple3) -> rule3)) -> rule5) OR ((((((triple1) -> rule4)) -> rule3)) -> rule5))]
("Erin" "is" "green" "-")
triple2
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is quiet.
True
2
proof
[(((triple3) -> rule3) OR ((((triple1) -> rule4)) -> rule3))]
("Erin" "is" "quiet" "+")
((triple3) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Harry is not round.
False
3
inv-proof
[(((triple6 triple7) -> rule7) OR ((((triple7) -> rule5) triple7) -> rule7))]
("Harry" "is" "round" "-")
((triple6 triple7) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple7) -> (rule5 % int2)) triple7) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Erin is round.
True
4
proof
[(((triple2 ((triple3) -> rule3)) -> rule7) OR ((triple2 ((((triple1) -> rule4)) -> rule3)) -> rule7) OR ((((((triple3) -> rule3)) -> rule5) ((triple3) -> rule3)) -> rule7) OR ((((((triple3) -> rule3)) -> rule5) ((((triple1) -> rule4)) -> rule3)) -> rule7) OR ((((((((triple1) -> rule4)) -> rule3)) -> rule5) ((triple3) -> rule3)) -> rule7) OR ((((((((triple1) -> rule4)) -> rule3)) -> rule5) ((((triple1) -> rule4)) -> rule3)) -> rule7))]
("Erin" "is" "round" "+")
((triple2 ((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((triple2 ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2)) ((triple3) -> (rule3 % int3))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple3) -> (rule3 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule4 % int2))) -> (rule3 % int4))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
((((((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((triple3) -> (rule3 % int3))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
((((((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Fiona is not quiet.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule3))]
("Fiona" "is" "quiet" "-")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is round.
True
5
proof
[(((triple5 ((((triple4) -> rule4)) -> rule3)) -> rule7) OR ((((((((triple4) -> rule4)) -> rule3)) -> rule5) ((((triple4) -> rule4)) -> rule3)) -> rule7))]
("Fiona" "is" "round" "+")
((triple5 ((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
((((((((triple4) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((((triple4) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is not round.
False
5
inv-proof
[(((triple5 ((((triple4) -> rule4)) -> rule3)) -> rule7) OR ((((((((triple4) -> rule4)) -> rule3)) -> rule5) ((((triple4) -> rule4)) -> rule3)) -> rule7))]
("Fiona" "is" "round" "-")
((triple5 ((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
((((((((triple4) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((((triple4) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Harry is not white.
Unknown
inv-rconc
[@2: Harry is white.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "cold" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Erin is cold.[(triple1)] Erin is green.[(triple2 OR ((((triple3) -> rule3)) -> rule5) OR ((((((triple1) -> rule4)) -> rule3)) -> rule5))] Erin is white.[(triple3 OR ((triple1) -> rule4))] Fiona is cold.[(triple4)] Fiona is green.[(triple5 OR ((((((triple4) -> rule4)) -> rule3)) -> rule5))] Harry is green.[(triple6 OR ((triple7) -> rule5))] Harry is quiet.[(triple7)] @1: Erin is quiet.[(((triple3) -> rule3) OR ((((triple1) -> rule4)) -> rule3))] Fiona is white.[(((triple4) -> rule4))] Harry is round.[(((triple6 triple7) -> rule7) OR ((((triple7) -> rule5) triple7) -> rule7))] @2: Erin is round.[(((triple2 ((triple3) -> rule3)) -> rule7) OR ((triple2 ((((triple1) -> rule4)) -> rule3)) -> rule7) OR ((((((triple3) -> rule3)) -> rule5) ((triple3) -> rule3)) -> rule7) OR ((((((triple3) -> rule3)) -> rule5) ((((triple1) -> rule4)) -> rule3)) -> rule7) OR ((((((((triple1) -> rule4)) -> rule3)) -> rule5) ((triple3) -> rule3)) -> rule7) OR ((((((((triple1) -> rule4)) -> rule3)) -> rule5) ((((triple1) -> rule4)) -> rule3)) -> rule7))] Fiona is quiet.[(((((triple4) -> rule4)) -> rule3))] @3: Fiona is round.[(((triple5 ((((triple4) -> rule4)) -> rule3)) -> rule7) OR ((((((((triple4) -> rule4)) -> rule3)) -> rule5) ((((triple4) -> rule4)) -> rule3)) -> rule7))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
triple3
((triple1) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
Fiona is green.
("Fiona" "is" "green" "+")
triple5
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
triple6
((triple7) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple3) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((triple4) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple6 triple7) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple7) -> (rule5 % int2)) triple7) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((triple2 ((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((triple2 ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2)) ((triple3) -> (rule3 % int3))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple3) -> (rule3 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule4 % int2))) -> (rule3 % int4))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
((((((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((triple3) -> (rule3 % int3))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
((((((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((triple5 ((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
((((((((triple4) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((((triple4) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4