Charlie is cold. Charlie is white. Fiona is red. Gary is cold. Gary is young. Harry is not cold. Harry is furry. White people are young. If someone is red and kind then they are young. White people are kind. All young people are not furry. All red people are nice. Cold people are white. Red, nice people are cold.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is furry.
("Harry" "is" "furry" "+")
White people are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If someone is red and kind then they are young.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
White people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
All young people are not furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "-"))
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Red, nice people are cold.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Charlie is cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "+")
triple1
Charlie is not cold.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "cold" "-")
triple1
Gary is not furry.
True
2
proof
[(((triple5) -> rule4) OR ((((((triple4) -> rule6)) -> rule1)) -> rule4))]
("Gary" "is" "furry" "-")
((triple5) -> (rule4 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
((((((triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Charlie is not young.
False
2
inv-proof
[(((triple2) -> rule1) OR ((((triple1) -> rule6)) -> rule1))]
("Charlie" "is" "young" "-")
((triple2) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Gary is kind.
True
3
proof
[(((((triple4) -> rule6)) -> rule3))]
("Gary" "is" "kind" "+")
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Fiona is not cold.
False
4
inv-proof
[(((triple3 ((triple3) -> rule5)) -> rule7))]
("Fiona" "is" "cold" "-")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is white.
True
5
proof
[(((((triple3 ((triple3) -> rule5)) -> rule7)) -> rule6))]
("Fiona" "is" "white" "+")
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is not white.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule5)) -> rule7)) -> rule6))]
("Fiona" "is" "white" "-")
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is kind.
True
6
proof
[(((((((triple3 ((triple3) -> rule5)) -> rule7)) -> rule6)) -> rule3))]
("Fiona" "is" "kind" "+")
((((((triple3 ((triple3) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is not young.
False
6
inv-proof
[(((((((triple3 ((triple3) -> rule5)) -> rule7)) -> rule6)) -> rule1) OR ((triple3 ((((((triple3 ((triple3) -> rule5)) -> rule7)) -> rule6)) -> rule3)) -> rule2))]
("Fiona" "is" "young" "-")
((((((triple3 ((triple3) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
((triple3 ((((((triple3 ((triple3) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
Fiona is not furry.
True
7
proof
[(((((((((triple3 ((triple3) -> rule5)) -> rule7)) -> rule6)) -> rule1)) -> rule4) OR ((((triple3 ((((((triple3 ((triple3) -> rule5)) -> rule7)) -> rule6)) -> rule3)) -> rule2)) -> rule4))]
("Fiona" "is" "furry" "-")
((((((((triple3 ((triple3) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
((((triple3 ((((((triple3 ((triple3) -> (rule5 % int6))) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
Fiona is nice.
("Fiona" "is" "nice" "+")
int6
Fiona is furry.
False
7
inv-proof
[(((((((((triple3 ((triple3) -> rule5)) -> rule7)) -> rule6)) -> rule1)) -> rule4) OR ((((triple3 ((((((triple3 ((triple3) -> rule5)) -> rule7)) -> rule6)) -> rule3)) -> rule2)) -> rule4))]
("Fiona" "is" "furry" "+")
((((((((triple3 ((triple3) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
((((triple3 ((((((triple3 ((triple3) -> (rule5 % int6))) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
Fiona is nice.
("Fiona" "is" "nice" "+")
int6
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "nice" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "nice" "+")
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is kind.
Unknown
rconc
[@2: Harry is kind.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is young.
Unknown
rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Harry" "is" "young" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Charlie is cold.[(triple1)] Charlie is white.[(triple2 OR ((triple1) -> rule6))] Fiona is red.[(triple3)] Gary is cold.[(triple4)] Gary is young.[(triple5 OR ((((triple4) -> rule6)) -> rule1))] Harry is furry.[(triple7)] Harry is not cold.[(triple6)] @1: Charlie is kind.[(((triple2) -> rule3) OR ((((triple1) -> rule6)) -> rule3))] Charlie is young.[(((triple2) -> rule1) OR ((((triple1) -> rule6)) -> rule1))] Fiona is nice.[(((triple3) -> rule5))] Gary is not furry.[(((triple5) -> rule4) OR ((((((triple4) -> rule6)) -> rule1)) -> rule4))] Gary is white.[(((triple4) -> rule6))] @2: Charlie is not furry.[(((((triple2) -> rule1)) -> rule4) OR ((((((triple1) -> rule6)) -> rule1)) -> rule4))] Fiona is cold.[(((triple3 ((triple3) -> rule5)) -> rule7))] Gary is kind.[(((((triple4) -> rule6)) -> rule3))] @3: Fiona is white.[(((((triple3 ((triple3) -> rule5)) -> rule7)) -> rule6))] @4: Fiona is kind.[(((((((triple3 ((triple3) -> rule5)) -> rule7)) -> rule6)) -> rule3))] Fiona is young.[(((((((triple3 ((triple3) -> rule5)) -> rule7)) -> rule6)) -> rule1) OR ((triple3 ((((((triple3 ((triple3) -> rule5)) -> rule7)) -> rule6)) -> rule3)) -> rule2))] @5: Fiona is not furry.[(((((((((triple3 ((triple3) -> rule5)) -> rule7)) -> rule6)) -> rule1)) -> rule4) OR ((((triple3 ((((((triple3 ((triple3) -> rule5)) -> rule7)) -> rule6)) -> rule3)) -> rule2)) -> rule4))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
((triple1) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is young.
("Gary" "is" "young" "+")
triple5
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is not cold.
("Harry" "is" "cold" "-")
triple6
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((triple2) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Gary is not furry.
("Gary" "is" "furry" "-")
((triple5) -> (rule4 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
((((((triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((triple4) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
((((((triple3 ((triple3) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
((((((triple3 ((triple3) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
((triple3 ((((((triple3 ((triple3) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
Fiona is not furry.
("Fiona" "is" "furry" "-")
((((((((triple3 ((triple3) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
((((triple3 ((((((triple3 ((triple3) -> (rule5 % int6))) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
Fiona is nice.
("Fiona" "is" "nice" "+")
int6