Bob is cold. Bob is not furry. Charlie is big. Charlie is quiet. Dave is not big. Erin is not big. Erin is white. Nice, rough things are quiet. Nice, big things are white. All big things are rough. Cold things are rough. All rough things are nice. If something is nice and quiet then it is big.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not furry.
("Bob" "is" "furry" "-")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is not big.
("Dave" "is" "big" "-")
Erin is not big.
("Erin" "is" "big" "-")
Erin is white.
("Erin" "is" "white" "+")
Nice, rough things are quiet.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Nice, big things are white.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
All big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is nice and quiet then it is big.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
Erin is not big.
True
1
proof
[(triple6)]
("Erin" "is" "big" "-")
triple6
Bob is furry.
False
1
inv-proof
[(triple2)]
("Bob" "is" "furry" "+")
triple2
Bob is rough.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple3) -> rule3))]
("Charlie" "is" "rough" "-")
((triple3) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
True
3
proof
[(((((triple3) -> rule3)) -> rule5))]
("Charlie" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not nice.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule5))]
("Charlie" "is" "nice" "-")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Bob is quiet.
True
6
proof
[(((((((triple1) -> rule4)) -> rule5) ((triple1) -> rule4)) -> rule1))]
("Bob" "is" "quiet" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2)) ((triple1) -> (rule4 % int3))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not quiet.
False
6
inv-proof
[(((((((triple1) -> rule4)) -> rule5) ((triple1) -> rule4)) -> rule1))]
("Bob" "is" "quiet" "-")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2)) ((triple1) -> (rule4 % int3))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is big.
True
10
proof
[(((((((triple1) -> rule4)) -> rule5) ((((((triple1) -> rule4)) -> rule5) ((triple1) -> rule4)) -> rule1)) -> rule6))]
("Bob" "is" "big" "+")
((((((triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((((((triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((triple1) -> (rule4 % int4))) -> (rule1 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is not big.
False
10
inv-proof
[(((((((triple1) -> rule4)) -> rule5) ((((((triple1) -> rule4)) -> rule5) ((triple1) -> rule4)) -> rule1)) -> rule6))]
("Bob" "is" "big" "-")
((((((triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((((((triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((triple1) -> (rule4 % int4))) -> (rule1 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is white.
True
14
proof
[(((((((triple1) -> rule4)) -> rule5) ((((((triple1) -> rule4)) -> rule5) ((((((triple1) -> rule4)) -> rule5) ((triple1) -> rule4)) -> rule1)) -> rule6)) -> rule2))]
("Bob" "is" "white" "+")
((((((triple1) -> (rule4 % int5))) -> (rule5 % int4)) ((((((triple1) -> (rule4 % int5))) -> (rule5 % int4)) ((((((triple1) -> (rule4 % int5))) -> (rule5 % int4)) ((triple1) -> (rule4 % int5))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is rough.
("Bob" "is" "rough" "+")
int5
Bob is not white.
False
14
inv-proof
[(((((((triple1) -> rule4)) -> rule5) ((((((triple1) -> rule4)) -> rule5) ((((((triple1) -> rule4)) -> rule5) ((triple1) -> rule4)) -> rule1)) -> rule6)) -> rule2))]
("Bob" "is" "white" "-")
((((((triple1) -> (rule4 % int5))) -> (rule5 % int4)) ((((((triple1) -> (rule4 % int5))) -> (rule5 % int4)) ((((((triple1) -> (rule4 % int5))) -> (rule5 % int4)) ((triple1) -> (rule4 % int5))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is rough.
("Bob" "is" "rough" "+")
int5
Dave is not nice.
Unknown
inv-rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Dave" "is" "nice" "-")
Erin is nice.
Unknown
rconc
[@2: Erin is nice.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Erin" "is" "nice" "+")
Erin is not quiet.
Unknown
inv-rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "rough" "+")
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "white" "-")
Dave is quiet.
Unknown
rconc
[@2: Dave is quiet.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Bob is cold.[(triple1)] Bob is not furry.[(triple2)] Charlie is big.[(triple3)] Charlie is quiet.[(triple4 OR ((((((triple3) -> rule3)) -> rule5) ((triple3) -> rule3)) -> rule1))] Dave is not big.[(triple5)] Erin is not big.[(triple6)] Erin is white.[(triple7)] @1: Bob is rough.[(((triple1) -> rule4))] Charlie is rough.[(((triple3) -> rule3))] @2: Bob is nice.[(((((triple1) -> rule4)) -> rule5))] Charlie is nice.[(((((triple3) -> rule3)) -> rule5))] @3: Bob is quiet.[(((((((triple1) -> rule4)) -> rule5) ((triple1) -> rule4)) -> rule1))] Charlie is white.[(((((((triple3) -> rule3)) -> rule5) triple3) -> rule2))] @4: Bob is big.[(((((((triple1) -> rule4)) -> rule5) ((((((triple1) -> rule4)) -> rule5) ((triple1) -> rule4)) -> rule1)) -> rule6))] @5: Bob is white.[(((((((triple1) -> rule4)) -> rule5) ((((((triple1) -> rule4)) -> rule5) ((((((triple1) -> rule4)) -> rule5) ((triple1) -> rule4)) -> rule1)) -> rule6)) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is not furry.
("Bob" "is" "furry" "-")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2)) ((triple3) -> (rule3 % int3))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Dave is not big.
("Dave" "is" "big" "-")
triple5
Erin is not big.
("Erin" "is" "big" "-")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple3) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2)) ((triple1) -> (rule4 % int3))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2)) triple3) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
((((((triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((((((triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((triple1) -> (rule4 % int4))) -> (rule1 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
((((((triple1) -> (rule4 % int5))) -> (rule5 % int4)) ((((((triple1) -> (rule4 % int5))) -> (rule5 % int4)) ((((((triple1) -> (rule4 % int5))) -> (rule5 % int4)) ((triple1) -> (rule4 % int5))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is rough.
("Bob" "is" "rough" "+")
int5