Bob is big. Bob is furry. Bob is smart. Bob is white. Charlie is quiet. Charlie is not smart. Fiona is not big. Fiona is furry. Fiona is quiet. Fiona is rough. Fiona is round. Fiona is smart. If someone is round then they are rough. All rough, big people are round. Furry people are round. If someone is rough then they are round. If someone is quiet then they are white. If someone is big and rough then they are quiet. If someone is big and not rough then they are quiet. If someone is smart and not big then they are quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Fiona is not big.
("Fiona" "is" "big" "-")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If someone is round then they are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All rough, big people are round.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
If someone is rough then they are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is big and rough then they are quiet.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If someone is big and not rough then they are quiet.
((("someone" "is" "big" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "quiet" "+"))
If someone is smart and not big then they are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "quiet" "+"))
Bob is smart.
True
1
proof
[(triple3)]
("Bob" "is" "smart" "+")
triple3
Bob is not smart.
False
1
inv-proof
[(triple3)]
("Bob" "is" "smart" "-")
triple3
Bob is round.
True
2
proof
[(((triple2) -> rule3))]
("Bob" "is" "round" "+")
((triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Fiona is not white.
False
2
inv-proof
[(((triple9) -> rule5) OR ((((triple12 triple7) -> rule8)) -> rule5))]
("Fiona" "is" "white" "-")
((triple9) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple12 triple7) -> (rule8 % int2))) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Bob is rough.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("Bob" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not rough.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("Bob" "is" "rough" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
True
5
proof
[(((triple1 ((((triple2) -> rule3)) -> rule1)) -> rule6))]
("Bob" "is" "quiet" "+")
((triple1 ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not quiet.
False
5
inv-proof
[(((triple1 ((((triple2) -> rule3)) -> rule1)) -> rule6))]
("Bob" "is" "quiet" "-")
((triple1 ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Charlie is not rough.
Unknown
inv-rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is round.
Unknown
rconc
[@3: Charlie is round.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Bob is big.[(triple1)] Bob is furry.[(triple2)] Bob is smart.[(triple3)] Bob is white.[(triple4 OR ((((triple1 ((((triple2) -> rule3)) -> rule1)) -> rule6)) -> rule5))] Charlie is not smart.[(triple6)] Charlie is quiet.[(triple5)] Fiona is furry.[(triple8)] Fiona is not big.[(triple7)] Fiona is quiet.[(triple9 OR ((triple12 triple7) -> rule8))] Fiona is rough.[(triple10 OR ((triple11) -> rule1) OR ((((triple8) -> rule3)) -> rule1))] Fiona is round.[(triple11 OR ((triple10) -> rule4) OR ((triple8) -> rule3))] Fiona is smart.[(triple12)] @1: Bob is round.[(((triple2) -> rule3))] Charlie is white.[(((triple5) -> rule5))] Fiona is white.[(((triple9) -> rule5) OR ((((triple12 triple7) -> rule8)) -> rule5))] @2: Bob is rough.[(((((triple2) -> rule3)) -> rule1))] @3: Bob is quiet.[(((triple1 ((((triple2) -> rule3)) -> rule1)) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
((((triple1 ((((triple2) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple6
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
Fiona is not big.
("Fiona" "is" "big" "-")
triple7
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
((triple12 triple7) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple10
((triple11) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
triple11
((triple10) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple8) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple5) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple9) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple12 triple7) -> (rule8 % int2))) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1 ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3