Dave is quiet. Dave is rough. Gary is furry. All quiet things are cold. Big things are smart. If something is cold then it is big. If something is quiet and round then it is big. All furry, round things are quiet. Round things are rough.
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is furry.
("Gary" "is" "furry" "+")
All quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something is quiet and round then it is big.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All furry, round things are quiet.
((("something" "is" "furry" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
Round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
Gary is furry.
True
1
proof
[(triple3)]
("Gary" "is" "furry" "+")
triple3
Gary is not furry.
False
1
inv-proof
[(triple3)]
("Gary" "is" "furry" "-")
triple3
Dave is cold.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Dave" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Dave" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is smart.
True
4
proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule2))]
("Dave" "is" "smart" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is not smart.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule2))]
("Dave" "is" "smart" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is cold.
Unknown
rconc
[@2: Gary is cold.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Gary" "is" "cold" "+")
Gary is not big.
Unknown
inv-rconc
[@3: Gary is big.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule5 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is smart.
Unknown
rconc
[@4: Gary is smart.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule1 <- rule5 <- FAIL)]]
("Gary" "is" "smart" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Dave is quiet.[(triple1)] Dave is rough.[(triple2)] Gary is furry.[(triple3)] @1: Dave is cold.[(((triple1) -> rule1))] @2: Dave is big.[(((((triple1) -> rule1)) -> rule3))] @3: Dave is smart.[(((((((triple1) -> rule1)) -> rule3)) -> rule2))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3