Charlie is nice. Dave is cold. Dave is not red. Dave is not rough. Dave is not smart. Gary is blue. Harry is big. Rough things are smart. Red, nice things are smart. All big things are rough. All nice, red things are rough. If Harry is smart and Harry is big then Harry is blue. If Charlie is red then Charlie is blue. All blue, smart things are nice. All nice, rough things are not cold.
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is not smart.
("Dave" "is" "smart" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is big.
("Harry" "is" "big" "+")
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Red, nice things are smart.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
All big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
All nice, red things are rough.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If Harry is smart and Harry is big then Harry is blue.
((("Harry" "is" "smart" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "blue" "+"))
If Charlie is red then Charlie is blue.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "blue" "+"))
All blue, smart things are nice.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
All nice, rough things are not cold.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "-"))
Dave is cold.
True
1
proof
[(triple2)]
("Dave" "is" "cold" "+")
triple2
Charlie is not nice.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "nice" "-")
triple1
Harry is rough.
True
2
proof
[(((triple7) -> rule3))]
("Harry" "is" "rough" "+")
((triple7) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple7) -> rule3))]
("Harry" "is" "rough" "-")
((triple7) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
True
3
proof
[(((((triple7) -> rule3)) -> rule1))]
("Harry" "is" "smart" "+")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not smart.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule1))]
("Harry" "is" "smart" "-")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is blue.
True
5
proof
[(((((((triple7) -> rule3)) -> rule1) triple7) -> rule5))]
("Harry" "is" "blue" "+")
((((((triple7) -> (rule3 % int3))) -> (rule1 % int2)) triple7) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not blue.
False
5
inv-proof
[(((((((triple7) -> rule3)) -> rule1) triple7) -> rule5))]
("Harry" "is" "blue" "-")
((((((triple7) -> (rule3 % int3))) -> (rule1 % int2)) triple7) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is nice.
True
9
proof
[(((((((((triple7) -> rule3)) -> rule1) triple7) -> rule5) ((((triple7) -> rule3)) -> rule1)) -> rule7))]
("Harry" "is" "nice" "+")
((((((((triple7) -> (rule3 % int4))) -> (rule1 % int3)) triple7) -> (rule5 % int2)) ((((triple7) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is not nice.
False
9
inv-proof
[(((((((((triple7) -> rule3)) -> rule1) triple7) -> rule5) ((((triple7) -> rule3)) -> rule1)) -> rule7))]
("Harry" "is" "nice" "-")
((((((((triple7) -> (rule3 % int4))) -> (rule1 % int3)) triple7) -> (rule5 % int2)) ((((triple7) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is not cold.
True
12
proof
[(((((((((((triple7) -> rule3)) -> rule1) triple7) -> rule5) ((((triple7) -> rule3)) -> rule1)) -> rule7) ((triple7) -> rule3)) -> rule8))]
("Harry" "is" "cold" "-")
((((((((((triple7) -> (rule3 % int5))) -> (rule1 % int4)) triple7) -> (rule5 % int3)) ((((triple7) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule7 % int2)) ((triple7) -> (rule3 % int5))) -> (rule8 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5
Harry is cold.
False
12
inv-proof
[(((((((((((triple7) -> rule3)) -> rule1) triple7) -> rule5) ((((triple7) -> rule3)) -> rule1)) -> rule7) ((triple7) -> rule3)) -> rule8))]
("Harry" "is" "cold" "+")
((((((((((triple7) -> (rule3 % int5))) -> (rule1 % int4)) triple7) -> (rule5 % int3)) ((((triple7) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule7 % int2)) ((triple7) -> (rule3 % int5))) -> (rule8 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5
Gary is not smart.
Unknown
inv-rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is nice.
Unknown
rconc
[@3: Gary is nice.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule3 <- FAIL)]]
("Gary" "is" "nice" "+")
Charlie is not smart.
Unknown
inv-rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Charlie" "is" "smart" "-")
Gary is rough.
Unknown
rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "rough" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "nice" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "blue" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Charlie is nice.[(triple1)] Dave is cold.[(triple2)] Dave is not red.[(triple3)] Dave is not rough.[(triple4)] Dave is not smart.[(triple5)] Gary is blue.[(triple6)] Harry is big.[(triple7)] @1: Harry is rough.[(((triple7) -> rule3))] @2: Harry is smart.[(((((triple7) -> rule3)) -> rule1))] @3: Harry is blue.[(((((((triple7) -> rule3)) -> rule1) triple7) -> rule5))] @4: Harry is nice.[(((((((((triple7) -> rule3)) -> rule1) triple7) -> rule5) ((((triple7) -> rule3)) -> rule1)) -> rule7))] @5: Harry is not cold.[(((((((((((triple7) -> rule3)) -> rule1) triple7) -> rule5) ((((triple7) -> rule3)) -> rule1)) -> rule7) ((triple7) -> rule3)) -> rule8))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is not red.
("Dave" "is" "red" "-")
triple3
Dave is not rough.
("Dave" "is" "rough" "-")
triple4
Dave is not smart.
("Dave" "is" "smart" "-")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is rough.
("Harry" "is" "rough" "+")
((triple7) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((((triple7) -> (rule3 % int3))) -> (rule1 % int2)) triple7) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((((((((triple7) -> (rule3 % int4))) -> (rule1 % int3)) triple7) -> (rule5 % int2)) ((((triple7) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is not cold.
("Harry" "is" "cold" "-")
((((((((((triple7) -> (rule3 % int5))) -> (rule1 % int4)) triple7) -> (rule5 % int3)) ((((triple7) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule7 % int2)) ((triple7) -> (rule3 % int5))) -> (rule8 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5