Bob is red. Dave is big. Dave is smart. If something is red then it is white. If something is cold then it is quiet. All smart things are big. If something is quiet then it is smart. If something is white then it is cold. All white things are cold.
Bob is red.
("Bob" "is" "red" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If something is red then it is white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If something is cold then it is quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If something is quiet then it is smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If something is white then it is cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
All white things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Bob is red.
True
1
proof
[(triple1)]
("Bob" "is" "red" "+")
triple1
Dave is not big.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule3))]
("Dave" "is" "big" "-")
triple2
((triple3) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Bob is white.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "white" "-")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is cold.
True
3
proof
[(((((triple1) -> rule1)) -> rule5) OR ((((triple1) -> rule1)) -> rule6))]
("Bob" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not cold.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5) OR ((((triple1) -> rule1)) -> rule6))]
("Bob" "is" "cold" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is quiet.
True
4
proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule2) OR ((((((triple1) -> rule1)) -> rule6)) -> rule2))]
("Bob" "is" "quiet" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not quiet.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule2) OR ((((((triple1) -> rule1)) -> rule6)) -> rule2))]
("Bob" "is" "quiet" "-")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "white" "-")
Dave is cold.
Unknown
rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not quiet.
Unknown
inv-rconc
[@3: Dave is quiet.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule1 <- FAIL)]]
("Dave" "is" "quiet" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Bob is red.[(triple1)] Dave is big.[(triple2 OR ((triple3) -> rule3))] Dave is smart.[(triple3)] @1: Bob is white.[(((triple1) -> rule1))] @2: Bob is cold.[(((((triple1) -> rule1)) -> rule5) OR ((((triple1) -> rule1)) -> rule6))] @3: Bob is quiet.[(((((((triple1) -> rule1)) -> rule5)) -> rule2) OR ((((((triple1) -> rule1)) -> rule6)) -> rule2))] @4: Bob is smart.[(((((((((triple1) -> rule1)) -> rule5)) -> rule2)) -> rule4) OR ((((((((triple1) -> rule1)) -> rule6)) -> rule2)) -> rule4))] @5: Bob is big.[(((((((((((triple1) -> rule1)) -> rule5)) -> rule2)) -> rule4)) -> rule3) OR ((((((((((triple1) -> rule1)) -> rule6)) -> rule2)) -> rule4)) -> rule3))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
((triple3) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((((((triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is big.
("Bob" "is" "big" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
((((((((((triple1) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5