Bob is kind. Fiona is round. Harry is big. If Bob is white then Bob is big. If something is big and not young then it is smart. Cold things are smart. Round things are cold. All round, smart things are cold. If Harry is kind then Harry is cold. If Fiona is young then Fiona is not big. All big, white things are not kind.
Bob is kind.
("Bob" "is" "kind" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
If Bob is white then Bob is big.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "big" "+"))
If something is big and not young then it is smart.
((("something" "is" "big" "+") ("something" "is" "young" "~")) -> ("something" "is" "smart" "+"))
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
All round, smart things are cold.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If Harry is kind then Harry is cold.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "cold" "+"))
If Fiona is young then Fiona is not big.
((("Fiona" "is" "young" "+")) -> ("Fiona" "is" "big" "-"))
All big, white things are not kind.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "-"))
Fiona is round.
True
1
proof
[(triple2)]
("Fiona" "is" "round" "+")
triple2
Harry is not big.
False
1
inv-proof
[(triple3)]
("Harry" "is" "big" "-")
triple3
Fiona is cold.
True
2
proof
[(((triple2) -> rule4))]
("Fiona" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is not cold.
False
2
inv-proof
[(((triple2) -> rule4))]
("Fiona" "is" "cold" "-")
((triple2) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
True
3
proof
[(((((triple2) -> rule4)) -> rule3))]
("Fiona" "is" "smart" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not smart.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule3))]
("Fiona" "is" "smart" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is smart.
Unknown
rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Bob" "is" "smart" "+")
Harry is not smart.
Unknown
inv-rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Harry" "is" "smart" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Bob is kind.[(triple1)] Fiona is round.[(triple2)] Harry is big.[(triple3)] @1: Fiona is cold.[(((triple2) -> rule4))] @2: Fiona is smart.[(((((triple2) -> rule4)) -> rule3))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Fiona is round.
("Fiona" "is" "round" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2