Bob is blue. Bob is smart. Fiona is cold. If Bob is round and Bob is not cold then Bob is not furry. Blue things are round. Cold things are big. Big things are rough. All rough, big things are smart. If Fiona is cold then Fiona is not round.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
If Bob is round and Bob is not cold then Bob is not furry.
((("Bob" "is" "round" "+") ("Bob" "is" "cold" "~")) -> ("Bob" "is" "furry" "-"))
Blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
All rough, big things are smart.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If Fiona is cold then Fiona is not round.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "round" "-"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Fiona is not cold.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "cold" "-")
triple3
Fiona is not round.
True
2
proof
[(((triple3) -> rule6))]
("Fiona" "is" "round" "-")
((triple3) -> (rule6 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Bob is not round.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "round" "-")
((triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Fiona is rough.
True
3
proof
[(((((triple3) -> rule3)) -> rule4))]
("Fiona" "is" "rough" "+")
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not rough.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule4))]
("Fiona" "is" "rough" "-")
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
True
6
proof
[(((((((triple3) -> rule3)) -> rule4) ((triple3) -> rule3)) -> rule5))]
("Fiona" "is" "smart" "+")
((((((triple3) -> (rule3 % int3))) -> (rule4 % int2)) ((triple3) -> (rule3 % int3))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is not smart.
False
6
inv-proof
[(((((((triple3) -> rule3)) -> rule4) ((triple3) -> rule3)) -> rule5))]
("Fiona" "is" "smart" "-")
((((((triple3) -> (rule3 % int3))) -> (rule4 % int2)) ((triple3) -> (rule3 % int3))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is rough.
Unknown
rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
@0: Bob is blue.[(triple1)] Bob is smart.[(triple2)] Fiona is cold.[(triple3)] @1: Bob is round.[(((triple1) -> rule2))] Fiona is big.[(((triple3) -> rule3))] Fiona is not round.[(((triple3) -> rule6))] @2: Fiona is rough.[(((((triple3) -> rule3)) -> rule4))] @3: Fiona is smart.[(((((((triple3) -> rule3)) -> rule4) ((triple3) -> rule3)) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple3) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not round.
("Fiona" "is" "round" "-")
((triple3) -> (rule6 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((((((triple3) -> (rule3 % int3))) -> (rule4 % int2)) ((triple3) -> (rule3 % int3))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3