Bob is big. Charlie is smart. Fiona is blue. If something is green and not young then it is smart. If Charlie is smart and Charlie is white then Charlie is round. If something is smart then it is white.
Bob is big.
("Bob" "is" "big" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
If something is green and not young then it is smart.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "is" "smart" "+"))
If Charlie is smart and Charlie is white then Charlie is round.
((("Charlie" "is" "smart" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "round" "+"))
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Fiona is blue.
True
1
proof
[(triple3)]
("Fiona" "is" "blue" "+")
triple3
Fiona is not blue.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "blue" "-")
triple3
Charlie is white.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "white" "+")
((triple2) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "white" "-")
((triple2) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
True
4
proof
[(((triple2 ((triple2) -> rule3)) -> rule2))]
("Charlie" "is" "round" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not round.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule2))]
("Charlie" "is" "round" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "smart" "-")
Bob is white.
Unknown
rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Bob" "is" "white" "+")
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is big.[(triple1)] Charlie is smart.[(triple2)] Fiona is blue.[(triple3)] @1: Charlie is white.[(((triple2) -> rule3))] @2: Charlie is round.[(((triple2 ((triple2) -> rule3)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2