Bob is nice. Bob is not quiet. Bob is smart. Charlie is big. Charlie is not nice. Dave is big. Fiona is not smart. Kind things are not big. Smart things are not round. If something is big then it is round. If Fiona is cold and Fiona is nice then Fiona is kind. If something is smart and kind then it is nice. If something is smart and not big then it is quiet. If something is big then it is quiet. Round, smart things are quiet.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Dave is big.
("Dave" "is" "big" "+")
Fiona is not smart.
("Fiona" "is" "smart" "-")
Kind things are not big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "-"))
Smart things are not round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "-"))
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If Fiona is cold and Fiona is nice then Fiona is kind.
((("Fiona" "is" "cold" "+") ("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "kind" "+"))
If something is smart and kind then it is nice.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is smart and not big then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "big" "~")) -> ("something" "is" "quiet" "+"))
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Round, smart things are quiet.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Bob is smart.
True
1
proof
[(triple3)]
("Bob" "is" "smart" "+")
triple3
Charlie is nice.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "nice" "+")
triple5
Bob is not round.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "round" "-")
((triple3) -> (rule2 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1
Charlie is not round.
False
2
inv-proof
[(((triple4) -> rule3))]
("Charlie" "is" "round" "-")
((triple4) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is round.
Unknown
rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "round" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is nice.[(triple1)] Bob is not quiet.[(triple2)] Bob is smart.[(triple3)] Charlie is big.[(triple4)] Charlie is not nice.[(triple5)] Dave is big.[(triple6)] Fiona is not smart.[(triple7)] @1: Bob is not round.[(((triple3) -> rule2))] Charlie is quiet.[(((triple4) -> rule7))] Charlie is round.[(((triple4) -> rule3))] Dave is quiet.[(((triple6) -> rule7))] Dave is round.[(((triple6) -> rule3))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Fiona is not smart.
("Fiona" "is" "smart" "-")
triple7
Bob is not round.
("Bob" "is" "round" "-")
((triple3) -> (rule2 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple4) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple4) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple6) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple6) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1