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