Bob is big. Bob is kind. Charlie is young. Fiona is green. Fiona is kind. Fiona is white. Harry is blue. If something is young and big then it is green. If Charlie is kind and Charlie is green then Charlie is white. If something is smart and white then it is kind. If something is kind then it is smart. Kind things are green. All big things are young. If something is big and young then it is smart. All kind, smart things are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If something is young and big then it is green.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If Charlie is kind and Charlie is green then Charlie is white.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "green" "+")) -> ("Charlie" "is" "white" "+"))
If something is smart and white then it is kind.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it is smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is big and young then it is smart.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
All kind, smart things are big.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Harry is blue.
True
1
proof
[(triple7)]
("Harry" "is" "blue" "+")
triple7
Bob is not big.
False
1
inv-proof
[(triple1 OR ((triple2 ((triple2) -> rule4)) -> rule8))]
("Bob" "is" "big" "-")
triple1
((triple2 ((triple2) -> (rule4 % int2))) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is green.
True
2
proof
[(((triple2) -> rule5) OR ((((triple1) -> rule6) triple1) -> rule1) OR ((((triple1) -> rule6) ((triple2 ((triple2) -> rule4)) -> rule8)) -> rule1) OR ((((((triple2 ((triple2) -> rule4)) -> rule8)) -> rule6) triple1) -> rule1) OR ((((((triple2 ((triple2) -> rule4)) -> rule8)) -> rule6) ((triple2 ((triple2) -> rule4)) -> rule8)) -> rule1))]
("Bob" "is" "green" "+")
((triple2) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple1) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple1) -> (rule6 % int4)) ((triple2 ((triple2) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
((((((triple2 ((triple2) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((triple2 ((triple2) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) ((triple2 ((triple2) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is not green.
False
2
inv-proof
[(((triple2) -> rule5) OR ((((triple1) -> rule6) triple1) -> rule1) OR ((((triple1) -> rule6) ((triple2 ((triple2) -> rule4)) -> rule8)) -> rule1) OR ((((((triple2 ((triple2) -> rule4)) -> rule8)) -> rule6) triple1) -> rule1) OR ((((((triple2 ((triple2) -> rule4)) -> rule8)) -> rule6) ((triple2 ((triple2) -> rule4)) -> rule8)) -> rule1))]
("Bob" "is" "green" "-")
((triple2) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple1) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple1) -> (rule6 % int4)) ((triple2 ((triple2) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
((((((triple2 ((triple2) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((triple2 ((triple2) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) ((triple2 ((triple2) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Fiona is big.
True
4
proof
[(((triple5 ((triple5) -> rule4)) -> rule8))]
("Fiona" "is" "big" "+")
((triple5 ((triple5) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is not big.
False
4
inv-proof
[(((triple5 ((triple5) -> rule4)) -> rule8))]
("Fiona" "is" "big" "-")
((triple5 ((triple5) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is young.
True
5
proof
[(((((triple5 ((triple5) -> rule4)) -> rule8)) -> rule6))]
("Fiona" "is" "young" "+")
((((triple5 ((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is not young.
False
5
inv-proof
[(((((triple5 ((triple5) -> rule4)) -> rule8)) -> rule6))]
("Fiona" "is" "young" "-")
((((triple5 ((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Harry is not green.
Unknown
inv-rconc
[@3: Harry is green.[CWA. Example of deepest failure = (rule1 <- rule8 <- rule3 <- FAIL)]]
("Harry" "is" "green" "-")
Harry is young.
Unknown
rconc
[@3: Harry is young.[CWA. Example of deepest failure = (rule6 <- rule8 <- rule3 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "kind" "-")
Charlie is big.
Unknown
rconc
[@3: Charlie is big.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "big" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is big.[(triple1 OR ((triple2 ((triple2) -> rule4)) -> rule8))] Bob is kind.[(triple2)] Charlie is young.[(triple3)] Fiona is green.[(triple4 OR ((triple5) -> rule5) OR ((((((triple5 ((triple5) -> rule4)) -> rule8)) -> rule6) ((triple5 ((triple5) -> rule4)) -> rule8)) -> rule1))] Fiona is kind.[(triple5)] Fiona is white.[(triple6)] Harry is blue.[(triple7)] @1: Bob is green.[(((triple2) -> rule5) OR ((((triple1) -> rule6) triple1) -> rule1) OR ((((triple1) -> rule6) ((triple2 ((triple2) -> rule4)) -> rule8)) -> rule1) OR ((((((triple2 ((triple2) -> rule4)) -> rule8)) -> rule6) triple1) -> rule1) OR ((((((triple2 ((triple2) -> rule4)) -> rule8)) -> rule6) ((triple2 ((triple2) -> rule4)) -> rule8)) -> rule1))] Bob is smart.[(((triple2) -> rule4) OR ((triple1 ((triple1) -> rule6)) -> rule7))] Bob is young.[(((triple1) -> rule6) OR ((((triple2 ((triple2) -> rule4)) -> rule8)) -> rule6))] Fiona is smart.[(((triple5) -> rule4))] @2: Fiona is big.[(((triple5 ((triple5) -> rule4)) -> rule8))] @3: Fiona is young.[(((((triple5 ((triple5) -> rule4)) -> rule8)) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2 ((triple2) -> (rule4 % int2))) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Fiona is green.
("Fiona" "is" "green" "+")
triple4
((triple5) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((((triple5 ((triple5) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) ((triple5 ((triple5) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
triple5
Fiona is white.
("Fiona" "is" "white" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple1) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple1) -> (rule6 % int4)) ((triple2 ((triple2) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
((((((triple2 ((triple2) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((triple2 ((triple2) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) ((triple2 ((triple2) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple1 ((triple1) -> (rule6 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple5) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple5 ((triple5) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((triple5 ((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3