Dave is nice. Dave is round. Dave is white. Fiona is kind. Fiona is red. Fiona is not white. Gary is red. Harry is kind. Harry is not nice. Harry is white. If something is red then it is green. All green things are cold. All red, white things are kind. Cold things are kind. If something is kind and cold then it is nice. If Fiona is round then Fiona is red. Nice things are round.
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is not white.
("Fiona" "is" "white" "-")
Gary is red.
("Gary" "is" "red" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is white.
("Harry" "is" "white" "+")
If something is red then it is green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
All red, white things are kind.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is kind and cold then it is nice.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If Fiona is round then Fiona is red.
((("Fiona" "is" "round" "+")) -> ("Fiona" "is" "red" "+"))
Nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Dave is white.
True
1
proof
[(triple3)]
("Dave" "is" "white" "+")
triple3
Fiona is white.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "white" "+")
triple6
Fiona is green.
True
2
proof
[(((triple5) -> rule1))]
("Fiona" "is" "green" "+")
((triple5) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple7) -> rule1))]
("Gary" "is" "green" "-")
((triple7) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Fiona is cold.
True
3
proof
[(((((triple5) -> rule1)) -> rule2))]
("Fiona" "is" "cold" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Gary is not cold.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule2))]
("Gary" "is" "cold" "-")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is kind.
True
4
proof
[(((((((triple7) -> rule1)) -> rule2)) -> rule4))]
("Gary" "is" "kind" "+")
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not kind.
False
4
inv-proof
[(((((((triple7) -> rule1)) -> rule2)) -> rule4))]
("Gary" "is" "kind" "-")
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Fiona is round.
True
6
proof
[(((((triple4 ((((triple5) -> rule1)) -> rule2)) -> rule5)) -> rule7) OR ((((((((((triple5) -> rule1)) -> rule2)) -> rule4) ((((triple5) -> rule1)) -> rule2)) -> rule5)) -> rule7))]
("Fiona" "is" "round" "+")
((((triple4 ((((triple5) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
((((((((((triple5) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple5) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
int5
Gary is not nice.
False
8
inv-proof
[(((((((((triple7) -> rule1)) -> rule2)) -> rule4) ((((triple7) -> rule1)) -> rule2)) -> rule5))]
("Gary" "is" "nice" "-")
((((((((triple7) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2)) ((((triple7) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is round.
True
9
proof
[(((((((((((triple7) -> rule1)) -> rule2)) -> rule4) ((((triple7) -> rule1)) -> rule2)) -> rule5)) -> rule7))]
("Gary" "is" "round" "+")
((((((((((triple7) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple7) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is green.
("Gary" "is" "green" "+")
int5
Gary is not round.
False
9
inv-proof
[(((((((((((triple7) -> rule1)) -> rule2)) -> rule4) ((((triple7) -> rule1)) -> rule2)) -> rule5)) -> rule7))]
("Gary" "is" "round" "-")
((((((((((triple7) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple7) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is green.
("Gary" "is" "green" "+")
int5
Dave is not kind.
Unknown
inv-rconc
[@3: Dave is kind.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule1 <- FAIL)]]
("Dave" "is" "kind" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "green" "+")
Dave is not cold.
Unknown
inv-rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Dave" "is" "cold" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "round" "+")
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Harry is cold.
Unknown
rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Harry" "is" "cold" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Dave is nice.[(triple1)] Dave is round.[(triple2 OR ((triple1) -> rule7))] Dave is white.[(triple3)] Fiona is kind.[(triple4 OR ((((((triple5) -> rule1)) -> rule2)) -> rule4))] Fiona is not white.[(triple6)] Fiona is red.[(triple5)] Gary is red.[(triple7)] Harry is kind.[(triple8)] Harry is not nice.[(triple9)] Harry is white.[(triple10)] @1: Fiona is green.[(((triple5) -> rule1))] Gary is green.[(((triple7) -> rule1))] @2: Fiona is cold.[(((((triple5) -> rule1)) -> rule2))] Gary is cold.[(((((triple7) -> rule1)) -> rule2))] @3: Fiona is nice.[(((triple4 ((((triple5) -> rule1)) -> rule2)) -> rule5) OR ((((((((triple5) -> rule1)) -> rule2)) -> rule4) ((((triple5) -> rule1)) -> rule2)) -> rule5))] Gary is kind.[(((((((triple7) -> rule1)) -> rule2)) -> rule4))] @4: Fiona is round.[(((((triple4 ((((triple5) -> rule1)) -> rule2)) -> rule5)) -> rule7) OR ((((((((((triple5) -> rule1)) -> rule2)) -> rule4) ((((triple5) -> rule1)) -> rule2)) -> rule5)) -> rule7))] Gary is nice.[(((((((((triple7) -> rule1)) -> rule2)) -> rule4) ((((triple7) -> rule1)) -> rule2)) -> rule5))] @5: Gary is round.[(((((((((((triple7) -> rule1)) -> rule2)) -> rule4) ((((triple7) -> rule1)) -> rule2)) -> rule5)) -> rule7))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
((triple1) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple3
Fiona is kind.
("Fiona" "is" "kind" "+")
triple4
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is not white.
("Fiona" "is" "white" "-")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple8
Harry is not nice.
("Harry" "is" "nice" "-")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Fiona is green.
("Fiona" "is" "green" "+")
((triple5) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple7) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple4 ((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
((((((((triple5) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2)) ((((triple5) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Gary is kind.
("Gary" "is" "kind" "+")
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
((((triple4 ((((triple5) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
((((((((((triple5) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple5) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
int5
Gary is nice.
("Gary" "is" "nice" "+")
((((((((triple7) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2)) ((((triple7) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is round.
("Gary" "is" "round" "+")
((((((((((triple7) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple7) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is green.
("Gary" "is" "green" "+")
int5