Bob is furry. Bob is red. Bob is rough. Bob is white. Bob is young. Charlie is furry. Charlie is kind. Charlie is red. Charlie is rough. Charlie is white. Fiona is furry. Fiona is kind. Fiona is red. Fiona is rough. Fiona is white. Fiona is young. All kind, young things are big. If something is kind and big then it is white. If something is white then it is furry. If something is big and kind then it is red. All big, furry things are young. All kind, young things are white. If something is kind and white then it is young. Kind things are white.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
All kind, young things are big.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If something is kind and big then it is white.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is white then it is furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If something is big and kind then it is red.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
All big, furry things are young.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
All kind, young things are white.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If something is kind and white then it is young.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Charlie is red.
True
1
proof
[(triple8 OR ((((triple7 ((triple7 triple10) -> rule7)) -> rule1) triple7) -> rule4) OR ((((triple7 ((triple7 ((triple7) -> rule8)) -> rule7)) -> rule1) triple7) -> rule4))]
("Charlie" "is" "red" "+")
triple8
((((triple7 ((triple7 triple10) -> (rule7 % int3))) -> (rule1 % int2)) triple7) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((triple7 ((triple7 ((triple7) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule1 % int2)) triple7) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is not red.
False
1
inv-proof
[(triple8 OR ((((triple7 ((triple7 triple10) -> rule7)) -> rule1) triple7) -> rule4) OR ((((triple7 ((triple7 ((triple7) -> rule8)) -> rule7)) -> rule1) triple7) -> rule4))]
("Charlie" "is" "red" "-")
triple8
((((triple7 ((triple7 triple10) -> (rule7 % int3))) -> (rule1 % int2)) triple7) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((triple7 ((triple7 ((triple7) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule1 % int2)) triple7) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is young.
True
3
proof
[(((triple7 triple10) -> rule7) OR ((triple7 ((triple7) -> rule8)) -> rule7))]
("Charlie" "is" "young" "+")
((triple7 triple10) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple7 ((triple7) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Fiona is not big.
False
3
inv-proof
[(((triple12 triple16) -> rule1) OR ((triple12 ((triple12 triple15) -> rule7)) -> rule1) OR ((triple12 ((triple12 ((triple12) -> rule8)) -> rule7)) -> rule1))]
("Fiona" "is" "big" "-")
((triple12 triple16) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple12 ((triple12 triple15) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((triple12 ((triple12 ((triple12) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Charlie is big.
True
5
proof
[(((triple7 ((triple7 triple10) -> rule7)) -> rule1) OR ((triple7 ((triple7 ((triple7) -> rule8)) -> rule7)) -> rule1))]
("Charlie" "is" "big" "+")
((triple7 ((triple7 triple10) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((triple7 ((triple7 ((triple7) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not big.
False
5
inv-proof
[(((triple7 ((triple7 triple10) -> rule7)) -> rule1) OR ((triple7 ((triple7 ((triple7) -> rule8)) -> rule7)) -> rule1))]
("Charlie" "is" "big" "-")
((triple7 ((triple7 triple10) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((triple7 ((triple7 ((triple7) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is furry.[(triple1 OR ((triple4) -> rule3))] Bob is red.[(triple2)] Bob is rough.[(triple3)] Bob is white.[(triple4)] Bob is young.[(triple5)] Charlie is furry.[(triple6 OR ((triple10) -> rule3) OR ((((triple7) -> rule8)) -> rule3))] Charlie is kind.[(triple7)] Charlie is red.[(triple8 OR ((((triple7 ((triple7 triple10) -> rule7)) -> rule1) triple7) -> rule4) OR ((((triple7 ((triple7 ((triple7) -> rule8)) -> rule7)) -> rule1) triple7) -> rule4))] Charlie is rough.[(triple9)] Charlie is white.[(triple10 OR ((triple7) -> rule8))] Fiona is furry.[(triple11 OR ((triple15) -> rule3) OR ((((triple12) -> rule8)) -> rule3) OR ((((triple12 triple16) -> rule6)) -> rule3) OR ((((triple12 ((triple12 triple16) -> rule1)) -> rule2)) -> rule3))] Fiona is kind.[(triple12)] Fiona is red.[(triple13 OR ((((triple12 triple16) -> rule1) triple12) -> rule4) OR ((((triple12 ((triple12 triple15) -> rule7)) -> rule1) triple12) -> rule4) OR ((((triple12 ((triple12 ((triple12) -> rule8)) -> rule7)) -> rule1) triple12) -> rule4))] Fiona is rough.[(triple14)] Fiona is white.[(triple15 OR ((triple12) -> rule8) OR ((triple12 triple16) -> rule6) OR ((triple12 ((triple12 triple16) -> rule1)) -> rule2))] Fiona is young.[(triple16 OR ((triple12 triple15) -> rule7) OR ((triple12 ((triple12) -> rule8)) -> rule7))] @1: Charlie is young.[(((triple7 triple10) -> rule7) OR ((triple7 ((triple7) -> rule8)) -> rule7))] Fiona is big.[(((triple12 triple16) -> rule1) OR ((triple12 ((triple12 triple15) -> rule7)) -> rule1) OR ((triple12 ((triple12 ((triple12) -> rule8)) -> rule7)) -> rule1))] @2: Charlie is big.[(((triple7 ((triple7 triple10) -> rule7)) -> rule1) OR ((triple7 ((triple7 ((triple7) -> rule8)) -> rule7)) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
((triple4) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
((triple10) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
triple8
((((triple7 ((triple7 triple10) -> (rule7 % int3))) -> (rule1 % int2)) triple7) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((triple7 ((triple7 ((triple7) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule1 % int2)) triple7) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple9
Charlie is white.
("Charlie" "is" "white" "+")
triple10
((triple7) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple11
((triple15) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple12) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((triple12 triple16) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((triple12 ((triple12 triple16) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
triple12
Fiona is red.
("Fiona" "is" "red" "+")
triple13
((((triple12 triple16) -> (rule1 % int2)) triple12) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((triple12 ((triple12 triple15) -> (rule7 % int3))) -> (rule1 % int2)) triple12) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((((triple12 ((triple12 ((triple12) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule1 % int2)) triple12) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is rough.
("Fiona" "is" "rough" "+")
triple14
Fiona is white.
("Fiona" "is" "white" "+")
triple15
((triple12) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple12 triple16) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple12 ((triple12 triple16) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
triple16
((triple12 triple15) -> (rule7 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple12 ((triple12) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((triple7 triple10) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple7 ((triple7) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((triple12 triple16) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple12 ((triple12 triple15) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((triple12 ((triple12 ((triple12) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
((triple7 ((triple7 triple10) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((triple7 ((triple7 ((triple7) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3