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