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