Bob is cold. Bob is quiet. Bob is not red. Charlie is furry. Fiona is rough. Harry is cold. Harry is green. All kind people are red. If Harry is red then Harry is kind. If someone is cold and green then they are rough. Rough people are kind. All red people are kind. Furry people are green. If Charlie is green and Charlie is furry then Charlie is cold.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not red.
("Bob" "is" "red" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
All kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If Harry is red then Harry is kind.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "kind" "+"))
If someone is cold and green then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
All red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
If Charlie is green and Charlie is furry then Charlie is cold.
((("Charlie" "is" "green" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "cold" "+"))
Bob is quiet.
True
1
proof
[(triple2)]
("Bob" "is" "quiet" "+")
triple2
Bob is not quiet.
False
1
inv-proof
[(triple2)]
("Bob" "is" "quiet" "-")
triple2
Fiona is kind.
True
2
proof
[(((triple5) -> rule4))]
("Fiona" "is" "kind" "+")
((triple5) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not kind.
False
2
inv-proof
[(((triple5) -> rule4))]
("Fiona" "is" "kind" "-")
((triple5) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
True
3
proof
[(((((triple5) -> rule4)) -> rule1))]
("Fiona" "is" "red" "+")
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not red.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule1))]
("Fiona" "is" "red" "-")
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Harry is red.
True
5
proof
[(((((((triple6 triple7) -> rule3)) -> rule4)) -> rule1))]
("Harry" "is" "red" "+")
((((((triple6 triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not red.
False
5
inv-proof
[(((((((triple6 triple7) -> rule3)) -> rule4)) -> rule1))]
("Harry" "is" "red" "-")
((((((triple6 triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Charlie is kind.
True
8
proof
[(((((((((triple4) -> rule6) triple4) -> rule7) ((triple4) -> rule6)) -> rule3)) -> rule4))]
("Charlie" "is" "kind" "+")
((((((((triple4) -> (rule6 % int4)) triple4) -> (rule7 % int3)) ((triple4) -> (rule6 % int4))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is not kind.
False
8
inv-proof
[(((((((((triple4) -> rule6) triple4) -> rule7) ((triple4) -> rule6)) -> rule3)) -> rule4))]
("Charlie" "is" "kind" "-")
((((((((triple4) -> (rule6 % int4)) triple4) -> (rule7 % int3)) ((triple4) -> (rule6 % int4))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is red.
True
9
proof
[(((((((((((triple4) -> rule6) triple4) -> rule7) ((triple4) -> rule6)) -> rule3)) -> rule4)) -> rule1))]
("Charlie" "is" "red" "+")
((((((((((triple4) -> (rule6 % int5)) triple4) -> (rule7 % int4)) ((triple4) -> (rule6 % int5))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is green.
("Charlie" "is" "green" "+")
int5
Charlie is not red.
False
9
inv-proof
[(((((((((((triple4) -> rule6) triple4) -> rule7) ((triple4) -> rule6)) -> rule3)) -> rule4)) -> rule1))]
("Charlie" "is" "red" "-")
((((((((((triple4) -> (rule6 % int5)) triple4) -> (rule7 % int4)) ((triple4) -> (rule6 % int5))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is green.
("Charlie" "is" "green" "+")
int5
Bob is not rough.
Unknown
inv-rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "green" "+")
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "green" "-")
Bob is kind.
Unknown
rconc
[@3: Bob is kind.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule6 <- FAIL)]]
("Bob" "is" "kind" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is cold.[(triple1)] Bob is not red.[(triple3)] Bob is quiet.[(triple2)] Charlie is furry.[(triple4)] Fiona is rough.[(triple5)] Harry is cold.[(triple6)] Harry is green.[(triple7)] @1: Charlie is green.[(((triple4) -> rule6))] Fiona is kind.[(((triple5) -> rule4))] Harry is rough.[(((triple6 triple7) -> rule3))] @2: Charlie is cold.[(((((triple4) -> rule6) triple4) -> rule7))] Fiona is red.[(((((triple5) -> rule4)) -> rule1))] Harry is kind.[(((((triple6 triple7) -> rule3)) -> rule4))] @3: Charlie is rough.[(((((((triple4) -> rule6) triple4) -> rule7) ((triple4) -> rule6)) -> rule3))] Harry is red.[(((((((triple6 triple7) -> rule3)) -> rule4)) -> rule1))] @4: Charlie is kind.[(((((((((triple4) -> rule6) triple4) -> rule7) ((triple4) -> rule6)) -> rule3)) -> rule4))] @5: Charlie is red.[(((((((((((triple4) -> rule6) triple4) -> rule7) ((triple4) -> rule6)) -> rule3)) -> rule4)) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is not red.
("Bob" "is" "red" "-")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple4) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple5) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple6 triple7) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple4) -> (rule6 % int2)) triple4) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple6 triple7) -> (rule3 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple4) -> (rule6 % int3)) triple4) -> (rule7 % int2)) ((triple4) -> (rule6 % int3))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((((triple6 triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((((triple4) -> (rule6 % int4)) triple4) -> (rule7 % int3)) ((triple4) -> (rule6 % int4))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
((((((((((triple4) -> (rule6 % int5)) triple4) -> (rule7 % int4)) ((triple4) -> (rule6 % int5))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is green.
("Charlie" "is" "green" "+")
int5