Bob is big. Bob is quiet. Bob is round. Bob is white. Charlie is big. Charlie is green. Dave is big. Dave is furry. Dave is green. Dave is quiet. Dave is round. Dave is smart. Dave is white. Fiona is green. Fiona is quiet. If someone is quiet then they are white.
Bob is big.
("Bob" "is" "big" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Bob is white.
True
1
proof
[(triple4 OR ((triple2) -> rule1))]
("Bob" "is" "white" "+")
triple4
((triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is not round.
False
1
inv-proof
[(triple11)]
("Dave" "is" "round" "-")
triple11
Fiona is white.
True
2
proof
[(((triple15) -> rule1))]
("Fiona" "is" "white" "+")
((triple15) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is not white.
False
2
inv-proof
[(((triple15) -> rule1))]
("Fiona" "is" "white" "-")
((triple15) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "white" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Bob is big.[(triple1)] Bob is quiet.[(triple2)] Bob is round.[(triple3)] Bob is white.[(triple4 OR ((triple2) -> rule1))] Charlie is big.[(triple5)] Charlie is green.[(triple6)] Dave is big.[(triple7)] Dave is furry.[(triple8)] Dave is green.[(triple9)] Dave is quiet.[(triple10)] Dave is round.[(triple11)] Dave is smart.[(triple12)] Dave is white.[(triple13 OR ((triple10) -> rule1))] Fiona is green.[(triple14)] Fiona is quiet.[(triple15)] @1: Fiona is white.[(((triple15) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
((triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Dave is big.
("Dave" "is" "big" "+")
triple7
Dave is furry.
("Dave" "is" "furry" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10
Dave is round.
("Dave" "is" "round" "+")
triple11
Dave is smart.
("Dave" "is" "smart" "+")
triple12
Dave is white.
("Dave" "is" "white" "+")
triple13
((triple10) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple14
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple15
Fiona is white.
("Fiona" "is" "white" "+")
((triple15) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1