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