Dave is not rough. Dave is white. Fiona is smart. Gary is blue. Gary is round. Gary is not white. Harry is round. Smart people are not nice. Red people are round. If someone is nice then they are red. If someone is rough then they are red. All white people are red. If Fiona is white then Fiona is rough. If Gary is blue then Gary is smart. Round people are blue. If someone is blue then they are smart.
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is white.
("Dave" "is" "white" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is not white.
("Gary" "is" "white" "-")
Harry is round.
("Harry" "is" "round" "+")
Smart people are not nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "-"))
Red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is nice then they are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone is rough then they are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
All white people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If Fiona is white then Fiona is rough.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "rough" "+"))
If Gary is blue then Gary is smart.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "smart" "+"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue then they are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Gary is not white.
True
1
proof
[(triple6)]
("Gary" "is" "white" "-")
triple6
Gary is not blue.
False
1
inv-proof
[(triple4 OR ((triple5) -> rule8))]
("Gary" "is" "blue" "-")
triple4
((triple5) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Harry is blue.
True
2
proof
[(((triple7) -> rule8))]
("Harry" "is" "blue" "+")
((triple7) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple7) -> rule8))]
("Harry" "is" "blue" "-")
((triple7) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Gary is not nice.
True
3
proof
[(((((triple4) -> rule7)) -> rule1) OR ((((triple4) -> rule9)) -> rule1) OR ((((((triple5) -> rule8)) -> rule7)) -> rule1) OR ((((((triple5) -> rule8)) -> rule9)) -> rule1))]
("Gary" "is" "nice" "-")
((((triple4) -> (rule7 % int2))) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple4) -> (rule9 % int2))) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((((triple5) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((((((triple5) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Harry is not smart.
False
3
inv-proof
[(((((triple7) -> rule8)) -> rule9))]
("Harry" "is" "smart" "-")
((((triple7) -> (rule8 % int2))) -> (rule9 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Dave is blue.
True
4
proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule8))]
("Dave" "is" "blue" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is not blue.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule8))]
("Dave" "is" "blue" "-")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is smart.
True
5
proof
[(((((((((triple2) -> rule5)) -> rule2)) -> rule8)) -> rule9))]
("Dave" "is" "smart" "+")
((((((((triple2) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is not smart.
False
5
inv-proof
[(((((((((triple2) -> rule5)) -> rule2)) -> rule8)) -> rule9))]
("Dave" "is" "smart" "-")
((((((((triple2) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is not nice.
True
6
proof
[(((((((((((triple2) -> rule5)) -> rule2)) -> rule8)) -> rule9)) -> rule1))]
("Dave" "is" "nice" "-")
((((((((((triple2) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5
Dave is nice.
False
6
inv-proof
[(((((((((((triple2) -> rule5)) -> rule2)) -> rule8)) -> rule9)) -> rule1))]
("Dave" "is" "nice" "+")
((((((((((triple2) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "rough" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "red" "+")
Fiona is not round.
Unknown
inv-rconc
[@3: Fiona is round.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule6 <- FAIL)]]
("Fiona" "is" "round" "-")
Harry is red.
Unknown
rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "red" "+")
Fiona is not red.
Unknown
inv-rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is blue.
Unknown
rconc
[@4: Fiona is blue.[CWA. Example of deepest failure = (rule8 <- rule2 <- rule4 <- rule6 <- FAIL)]]
("Fiona" "is" "blue" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Dave is not rough.[(triple1)] Dave is white.[(triple2)] Fiona is smart.[(triple3)] Gary is blue.[(triple4 OR ((triple5) -> rule8))] Gary is not white.[(triple6)] Gary is round.[(triple5)] Harry is round.[(triple7)] @1: Dave is red.[(((triple2) -> rule5))] Fiona is not nice.[(((triple3) -> rule1))] Gary is smart.[(((triple4) -> rule7) OR ((triple4) -> rule9) OR ((((triple5) -> rule8)) -> rule7) OR ((((triple5) -> rule8)) -> rule9))] Harry is blue.[(((triple7) -> rule8))] @2: Dave is round.[(((((triple2) -> rule5)) -> rule2))] Gary is not nice.[(((((triple4) -> rule7)) -> rule1) OR ((((triple4) -> rule9)) -> rule1) OR ((((((triple5) -> rule8)) -> rule7)) -> rule1) OR ((((((triple5) -> rule8)) -> rule9)) -> rule1))] Harry is smart.[(((((triple7) -> rule8)) -> rule9))] @3: Dave is blue.[(((((((triple2) -> rule5)) -> rule2)) -> rule8))] Harry is not nice.[(((((((triple7) -> rule8)) -> rule9)) -> rule1))] @4: Dave is smart.[(((((((((triple2) -> rule5)) -> rule2)) -> rule8)) -> rule9))] @5: Dave is not nice.[(((((((((((triple2) -> rule5)) -> rule2)) -> rule8)) -> rule9)) -> rule1))]
Dave is not rough.
("Dave" "is" "rough" "-")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
((triple5) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
((triple2) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Fiona is not nice.
("Fiona" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple4) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple4) -> (rule9 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple5) -> (rule8 % int2))) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple5) -> (rule8 % int2))) -> (rule9 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Gary is not nice.
("Gary" "is" "nice" "-")
((((triple4) -> (rule7 % int2))) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple4) -> (rule9 % int2))) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((((triple5) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((((((triple5) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((((triple7) -> (rule8 % int2))) -> (rule9 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Harry is not nice.
("Harry" "is" "nice" "-")
((((((triple7) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((((((((triple2) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is not nice.
("Dave" "is" "nice" "-")
((((((((((triple2) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5