Anne is smart. Anne is white. Charlie is big. Charlie is kind. Charlie is nice. Charlie is round. Charlie is white. Dave is kind. Dave is round. Dave is white. Fiona is big. Fiona is cold. Fiona is nice. Fiona is white. All cold things are round. Smart things are round. All cold, white things are big. If something is big then it is nice. If something is smart and kind then it is cold. All cold, round things are smart. If Dave is kind and Dave is white then Dave is round. If something is cold then it is kind. All round things are kind.
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is white.
("Fiona" "is" "white" "+")
All cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
All cold, white things are big.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is big then it is nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is smart and kind then it is cold.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
All cold, round things are smart.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If Dave is kind and Dave is white then Dave is round.
((("Dave" "is" "kind" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "round" "+"))
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
All round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Charlie is big.
True
1
proof
[(triple3)]
("Charlie" "is" "big" "+")
triple3
Anne is not white.
False
1
inv-proof
[(triple2)]
("Anne" "is" "white" "-")
triple2
Fiona is round.
True
2
proof
[(((triple12) -> rule1))]
("Fiona" "is" "round" "+")
((triple12) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is not kind.
False
2
inv-proof
[(((triple12) -> rule8) OR ((((triple12) -> rule1)) -> rule9))]
("Fiona" "is" "kind" "-")
((triple12) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule9 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is smart.
True
4
proof
[(((triple12 ((triple12) -> rule1)) -> rule6))]
("Fiona" "is" "smart" "+")
((triple12 ((triple12) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Anne is not kind.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule9))]
("Anne" "is" "kind" "-")
((((triple1) -> (rule2 % int2))) -> (rule9 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is cold.
True
5
proof
[(((triple1 ((((triple1) -> rule2)) -> rule9)) -> rule5))]
("Anne" "is" "cold" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not cold.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule2)) -> rule9)) -> rule5))]
("Anne" "is" "cold" "-")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is big.
True
7
proof
[(((((triple1 ((((triple1) -> rule2)) -> rule9)) -> rule5) triple2) -> rule3))]
("Anne" "is" "big" "+")
((((triple1 ((((triple1) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is not big.
False
7
inv-proof
[(((((triple1 ((((triple1) -> rule2)) -> rule9)) -> rule5) triple2) -> rule3))]
("Anne" "is" "big" "-")
((((triple1 ((((triple1) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is nice.
True
8
proof
[(((((((triple1 ((((triple1) -> rule2)) -> rule9)) -> rule5) triple2) -> rule3)) -> rule4))]
("Anne" "is" "nice" "+")
((((((triple1 ((((triple1) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule5 % int3)) triple2) -> (rule3 % int2))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Anne is not nice.
False
8
inv-proof
[(((((((triple1 ((((triple1) -> rule2)) -> rule9)) -> rule5) triple2) -> rule3)) -> rule4))]
("Anne" "is" "nice" "-")
((((((triple1 ((((triple1) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule5 % int3)) triple2) -> (rule3 % int2))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Charlie is not smart.
Unknown
inv-rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Charlie" "is" "smart" "-")
Dave is cold.
Unknown
rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not smart.
Unknown
inv-rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Dave" "is" "smart" "-")
Charlie is cold.
Unknown
rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Charlie" "is" "cold" "+")
Dave is not big.
Unknown
inv-rconc
[@3: Dave is big.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule6 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is nice.
Unknown
rconc
[@4: Dave is nice.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule5 <- rule6 <- FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is smart.[(triple1)] Anne is white.[(triple2)] Charlie is big.[(triple3)] Charlie is kind.[(triple4 OR ((triple6) -> rule9))] Charlie is nice.[(triple5 OR ((triple3) -> rule4))] Charlie is round.[(triple6)] Charlie is white.[(triple7)] Dave is kind.[(triple8 OR ((triple9) -> rule9))] Dave is round.[(triple9 OR ((triple8 triple10) -> rule7))] Dave is white.[(triple10)] Fiona is big.[(triple11 OR ((triple12 triple14) -> rule3))] Fiona is cold.[(triple12)] Fiona is nice.[(triple13 OR ((triple11) -> rule4) OR ((((triple12 triple14) -> rule3)) -> rule4))] Fiona is white.[(triple14)] @1: Anne is round.[(((triple1) -> rule2))] Fiona is kind.[(((triple12) -> rule8) OR ((((triple12) -> rule1)) -> rule9))] Fiona is round.[(((triple12) -> rule1))] @2: Anne is kind.[(((((triple1) -> rule2)) -> rule9))] Fiona is smart.[(((triple12 ((triple12) -> rule1)) -> rule6))] @3: Anne is cold.[(((triple1 ((((triple1) -> rule2)) -> rule9)) -> rule5))] @4: Anne is big.[(((((triple1 ((((triple1) -> rule2)) -> rule9)) -> rule5) triple2) -> rule3))] @5: Anne is nice.[(((((((triple1 ((((triple1) -> rule2)) -> rule9)) -> rule5) triple2) -> rule3)) -> rule4))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
((triple6) -> (rule9 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
((triple3) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Dave is kind.
("Dave" "is" "kind" "+")
triple8
((triple9) -> (rule9 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple9
((triple8 triple10) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple10
Fiona is big.
("Fiona" "is" "big" "+")
triple11
((triple12 triple14) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple12
Fiona is nice.
("Fiona" "is" "nice" "+")
triple13
((triple11) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple12 triple14) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
triple14
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple12) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule9 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((triple12) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule9 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple12 ((triple12) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
((((triple1 ((((triple1) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple1 ((((triple1) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule5 % int3)) triple2) -> (rule3 % int2))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5