Bob is white. Fiona is white. Harry is not quiet. If something is young then it is not round. Rough things are round. If Bob is round then Bob is cold. If Fiona is white then Fiona is cold. All white things are rough. Young, round things are rough. All cold things are rough. If Fiona is rough then Fiona is quiet.
Bob is white.
("Bob" "is" "white" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
If something is young then it is not round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "-"))
Rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If Bob is round then Bob is cold.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "cold" "+"))
If Fiona is white then Fiona is cold.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "cold" "+"))
All white things are rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
Young, round things are rough.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
All cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If Fiona is rough then Fiona is quiet.
((("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "quiet" "+"))
Harry is not quiet.
True
1
proof
[(triple3)]
("Harry" "is" "quiet" "-")
triple3
Harry is quiet.
False
1
inv-proof
[(triple3)]
("Harry" "is" "quiet" "+")
triple3
Fiona is rough.
True
2
proof
[(((triple2) -> rule5) OR ((((triple2) -> rule4)) -> rule7))]
("Fiona" "is" "rough" "+")
((triple2) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not rough.
False
2
inv-proof
[(((triple2) -> rule5) OR ((((triple2) -> rule4)) -> rule7))]
("Fiona" "is" "rough" "-")
((triple2) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is quiet.
True
3
proof
[(((((triple2) -> rule5)) -> rule8) OR ((((((triple2) -> rule4)) -> rule7)) -> rule8))]
("Fiona" "is" "quiet" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is not quiet.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule8) OR ((((((triple2) -> rule4)) -> rule7)) -> rule8))]
("Fiona" "is" "quiet" "-")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Bob is cold.
True
4
proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule3))]
("Bob" "is" "cold" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not cold.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule3))]
("Bob" "is" "cold" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is round.
Unknown
rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Harry" "is" "round" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Bob is white.[(triple1)] Fiona is white.[(triple2)] Harry is not quiet.[(triple3)] @1: Bob is rough.[(((triple1) -> rule5))] Fiona is cold.[(((triple2) -> rule4))] Fiona is rough.[(((triple2) -> rule5) OR ((((triple2) -> rule4)) -> rule7))] @2: Bob is round.[(((((triple1) -> rule5)) -> rule2))] Fiona is quiet.[(((((triple2) -> rule5)) -> rule8) OR ((((((triple2) -> rule4)) -> rule7)) -> rule8))] Fiona is round.[(((((triple2) -> rule5)) -> rule2) OR ((((((triple2) -> rule4)) -> rule7)) -> rule2))] @3: Bob is cold.[(((((((triple1) -> rule5)) -> rule2)) -> rule3))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Fiona is white.
("Fiona" "is" "white" "+")
triple2
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple2) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3