Dave is white. Fiona is cold. Gary is cold. Gary is green. Harry is blue. Harry is green. Harry is white. If something is smart and kind then it is red. White, cold things are blue. If something is blue then it is green. If something is smart then it is white. Blue things are smart. If something is cold then it is white. If Fiona is smart and Fiona is blue then Fiona is kind.
Dave is white.
("Dave" "is" "white" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is smart and kind then it is red.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
White, cold things are blue.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If something is cold then it is white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If Fiona is smart and Fiona is blue then Fiona is kind.
((("Fiona" "is" "smart" "+") ("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "kind" "+"))
Gary is green.
True
1
proof
[(triple4 OR ((((((triple3) -> rule6) triple3) -> rule2)) -> rule3))]
("Gary" "is" "green" "+")
triple4
((((((triple3) -> (rule6 % int3)) triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Harry is not blue.
False
1
inv-proof
[(triple5)]
("Harry" "is" "blue" "-")
triple5
Fiona is white.
True
2
proof
[(((triple2) -> rule6))]
("Fiona" "is" "white" "+")
((triple2) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is not white.
False
2
inv-proof
[(((triple2) -> rule6))]
("Fiona" "is" "white" "-")
((triple2) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Gary is blue.
True
4
proof
[(((((triple3) -> rule6) triple3) -> rule2))]
("Gary" "is" "blue" "+")
((((triple3) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not blue.
False
4
inv-proof
[(((((triple3) -> rule6) triple3) -> rule2))]
("Gary" "is" "blue" "-")
((((triple3) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Fiona is smart.
True
5
proof
[(((((((triple2) -> rule6) triple2) -> rule2)) -> rule5))]
("Fiona" "is" "smart" "+")
((((((triple2) -> (rule6 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Gary is not smart.
False
5
inv-proof
[(((((((triple3) -> rule6) triple3) -> rule2)) -> rule5))]
("Gary" "is" "smart" "-")
((((((triple3) -> (rule6 % int3)) triple3) -> (rule2 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Fiona is kind.
True
10
proof
[(((((((((triple2) -> rule6) triple2) -> rule2)) -> rule5) ((((triple2) -> rule6) triple2) -> rule2)) -> rule7))]
("Fiona" "is" "kind" "+")
((((((((triple2) -> (rule6 % int4)) triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple2) -> (rule6 % int4)) triple2) -> (rule2 % int3))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is not kind.
False
10
inv-proof
[(((((((((triple2) -> rule6) triple2) -> rule2)) -> rule5) ((((triple2) -> rule6) triple2) -> rule2)) -> rule7))]
("Fiona" "is" "kind" "-")
((((((((triple2) -> (rule6 % int4)) triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple2) -> (rule6 % int4)) triple2) -> (rule2 % int3))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is red.
True
16
proof
[(((((((((triple2) -> rule6) triple2) -> rule2)) -> rule5) ((((((((triple2) -> rule6) triple2) -> rule2)) -> rule5) ((((triple2) -> rule6) triple2) -> rule2)) -> rule7)) -> rule1))]
("Fiona" "is" "red" "+")
((((((((triple2) -> (rule6 % int5)) triple2) -> (rule2 % int4))) -> (rule5 % int3)) ((((((((triple2) -> (rule6 % int5)) triple2) -> (rule2 % int4))) -> (rule5 % int3)) ((((triple2) -> (rule6 % int5)) triple2) -> (rule2 % int4))) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
int5
Fiona is not red.
False
16
inv-proof
[(((((((((triple2) -> rule6) triple2) -> rule2)) -> rule5) ((((((((triple2) -> rule6) triple2) -> rule2)) -> rule5) ((((triple2) -> rule6) triple2) -> rule2)) -> rule7)) -> rule1))]
("Fiona" "is" "red" "-")
((((((((triple2) -> (rule6 % int5)) triple2) -> (rule2 % int4))) -> (rule5 % int3)) ((((((((triple2) -> (rule6 % int5)) triple2) -> (rule2 % int4))) -> (rule5 % int3)) ((((triple2) -> (rule6 % int5)) triple2) -> (rule2 % int4))) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
int5
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "red" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "red" "+")
Dave is not green.
Unknown
inv-rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is smart.
Unknown
rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Dave" "is" "smart" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "red" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "blue" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Dave is white.[(triple1)] Fiona is cold.[(triple2)] Gary is cold.[(triple3)] Gary is green.[(triple4 OR ((((((triple3) -> rule6) triple3) -> rule2)) -> rule3))] Harry is blue.[(triple5)] Harry is green.[(triple6 OR ((triple5) -> rule3))] Harry is white.[(triple7 OR ((((triple5) -> rule5)) -> rule4))] @1: Fiona is white.[(((triple2) -> rule6))] Gary is white.[(((triple3) -> rule6))] Harry is smart.[(((triple5) -> rule5))] @2: Fiona is blue.[(((((triple2) -> rule6) triple2) -> rule2))] Gary is blue.[(((((triple3) -> rule6) triple3) -> rule2))] @3: Fiona is green.[(((((((triple2) -> rule6) triple2) -> rule2)) -> rule3))] Fiona is smart.[(((((((triple2) -> rule6) triple2) -> rule2)) -> rule5))] Gary is smart.[(((((((triple3) -> rule6) triple3) -> rule2)) -> rule5))] @4: Fiona is kind.[(((((((((triple2) -> rule6) triple2) -> rule2)) -> rule5) ((((triple2) -> rule6) triple2) -> rule2)) -> rule7))] @5: Fiona is red.[(((((((((triple2) -> rule6) triple2) -> rule2)) -> rule5) ((((((((triple2) -> rule6) triple2) -> rule2)) -> rule5) ((((triple2) -> rule6) triple2) -> rule2)) -> rule7)) -> rule1))]
Dave is white.
("Dave" "is" "white" "+")
triple1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple4
((((((triple3) -> (rule6 % int3)) triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
((triple5) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple7
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((triple2) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple5) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple2) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple3) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((((((triple2) -> (rule6 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((((((triple2) -> (rule6 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((((((triple3) -> (rule6 % int3)) triple3) -> (rule2 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
((((((((triple2) -> (rule6 % int4)) triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple2) -> (rule6 % int4)) triple2) -> (rule2 % int3))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is red.
("Fiona" "is" "red" "+")
((((((((triple2) -> (rule6 % int5)) triple2) -> (rule2 % int4))) -> (rule5 % int3)) ((((((((triple2) -> (rule6 % int5)) triple2) -> (rule2 % int4))) -> (rule5 % int3)) ((((triple2) -> (rule6 % int5)) triple2) -> (rule2 % int4))) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
int5