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