Bob is nice. Charlie is quiet. Dave is green. Fiona is cold. Fiona is green. Fiona is kind. Fiona is quiet. If someone is cold and white then they are not green. All green people are kind. Cold people are quiet. All white, nice people are quiet. If Bob is cold and Bob is furry then Bob is white. Quiet, cold people are furry. All nice people are cold. If Fiona is quiet and Fiona is white then Fiona is not nice.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is green.
("Dave" "is" "green" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If someone is cold and white then they are not green.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "-"))
All green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
All white, nice people are quiet.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is cold and Bob is furry then Bob is white.
((("Bob" "is" "cold" "+") ("Bob" "is" "furry" "+")) -> ("Bob" "is" "white" "+"))
Quiet, cold people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
All nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If Fiona is quiet and Fiona is white then Fiona is not nice.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "white" "+")) -> ("Fiona" "is" "nice" "-"))
Charlie is quiet.
True
1
proof
[(triple2)]
("Charlie" "is" "quiet" "+")
triple2
Fiona is not kind.
False
1
inv-proof
[(triple6 OR ((triple5) -> rule2))]
("Fiona" "is" "kind" "-")
triple6
((triple5) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Dave is kind.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "kind" "-")
((triple3) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Bob is quiet.
True
3
proof
[(((((triple1) -> rule7)) -> rule3))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not quiet.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule3))]
("Bob" "is" "quiet" "-")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
True
6
proof
[(((((((triple1) -> rule7)) -> rule3) ((triple1) -> rule7)) -> rule6))]
("Bob" "is" "furry" "+")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2)) ((triple1) -> (rule7 % int3))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not furry.
False
6
inv-proof
[(((((((triple1) -> rule7)) -> rule3) ((triple1) -> rule7)) -> rule6))]
("Bob" "is" "furry" "-")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2)) ((triple1) -> (rule7 % int3))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is white.
True
9
proof
[(((((triple1) -> rule7) ((((((triple1) -> rule7)) -> rule3) ((triple1) -> rule7)) -> rule6)) -> rule5))]
("Bob" "is" "white" "+")
((((triple1) -> (rule7 % int4)) ((((((triple1) -> (rule7 % int4))) -> (rule3 % int3)) ((triple1) -> (rule7 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Bob is not white.
False
9
inv-proof
[(((((triple1) -> rule7) ((((((triple1) -> rule7)) -> rule3) ((triple1) -> rule7)) -> rule6)) -> rule5))]
("Bob" "is" "white" "-")
((((triple1) -> (rule7 % int4)) ((((((triple1) -> (rule7 % int4))) -> (rule3 % int3)) ((triple1) -> (rule7 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Bob is not green.
True
12
proof
[(((((triple1) -> rule7) ((((triple1) -> rule7) ((((((triple1) -> rule7)) -> rule3) ((triple1) -> rule7)) -> rule6)) -> rule5)) -> rule1))]
("Bob" "is" "green" "-")
((((triple1) -> (rule7 % int5)) ((((triple1) -> (rule7 % int5)) ((((((triple1) -> (rule7 % int5))) -> (rule3 % int4)) ((triple1) -> (rule7 % int5))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is cold.
("Bob" "is" "cold" "+")
int5
Bob is green.
False
12
inv-proof
[(((((triple1) -> rule7) ((((triple1) -> rule7) ((((((triple1) -> rule7)) -> rule3) ((triple1) -> rule7)) -> rule6)) -> rule5)) -> rule1))]
("Bob" "is" "green" "+")
((((triple1) -> (rule7 % int5)) ((((triple1) -> (rule7 % int5)) ((((((triple1) -> (rule7 % int5))) -> (rule3 % int4)) ((triple1) -> (rule7 % int5))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is cold.
("Bob" "is" "cold" "+")
int5
Dave is not quiet.
Unknown
inv-rconc
[@2: Dave is quiet.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("Dave" "is" "quiet" "-")
Charlie is furry.
Unknown
rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Charlie" "is" "furry" "+")
Dave is not furry.
Unknown
inv-rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Dave" "is" "furry" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "kind" "+")
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "cold" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Bob is nice.[(triple1)] Charlie is quiet.[(triple2)] Dave is green.[(triple3)] Fiona is cold.[(triple4)] Fiona is green.[(triple5)] Fiona is kind.[(triple6 OR ((triple5) -> rule2))] Fiona is quiet.[(triple7 OR ((triple4) -> rule3))] @1: Bob is cold.[(((triple1) -> rule7))] Dave is kind.[(((triple3) -> rule2))] Fiona is furry.[(((triple7 triple4) -> rule6) OR ((((triple4) -> rule3) triple4) -> rule6))] @2: Bob is quiet.[(((((triple1) -> rule7)) -> rule3))] @3: Bob is furry.[(((((((triple1) -> rule7)) -> rule3) ((triple1) -> rule7)) -> rule6))] @4: Bob is white.[(((((triple1) -> rule7) ((((((triple1) -> rule7)) -> rule3) ((triple1) -> rule7)) -> rule6)) -> rule5))] @5: Bob is not green.[(((((triple1) -> rule7) ((((triple1) -> rule7) ((((((triple1) -> rule7)) -> rule3) ((triple1) -> rule7)) -> rule6)) -> rule5)) -> rule1))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
Fiona is green.
("Fiona" "is" "green" "+")
triple5
Fiona is kind.
("Fiona" "is" "kind" "+")
triple6
((triple5) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
((triple4) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple7 triple4) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple4) -> (rule3 % int2)) triple4) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2)) ((triple1) -> (rule7 % int3))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule7 % int4)) ((((((triple1) -> (rule7 % int4))) -> (rule3 % int3)) ((triple1) -> (rule7 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Bob is not green.
("Bob" "is" "green" "-")
((((triple1) -> (rule7 % int5)) ((((triple1) -> (rule7 % int5)) ((((((triple1) -> (rule7 % int5))) -> (rule3 % int4)) ((triple1) -> (rule7 % int5))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is cold.
("Bob" "is" "cold" "+")
int5