Dave is big. Dave is green. Dave is red. Dave is smart. Dave is white. Fiona is green. Fiona is kind. Fiona is white. Gary is green. Gary is smart. Harry is white. Harry is young. If someone is smart and white then they are green. If someone is kind then they are smart. All red people are big. All big, red people are kind. If Dave is big then Dave is smart. If someone is young then they are red.
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is smart and white then they are green.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If someone is kind then they are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
All big, red people are kind.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If Dave is big then Dave is smart.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "smart" "+"))
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
Dave is big.
True
1
proof
[(triple1 OR ((triple3) -> rule3))]
("Dave" "is" "big" "+")
triple1
((triple3) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Harry is not young.
False
1
inv-proof
[(triple12)]
("Harry" "is" "young" "-")
triple12
Fiona is smart.
True
2
proof
[(((triple7) -> rule2))]
("Fiona" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple7) -> rule2))]
("Fiona" "is" "smart" "-")
((triple7) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is big.
True
3
proof
[(((((triple12) -> rule6)) -> rule3))]
("Harry" "is" "big" "+")
((((triple12) -> (rule6 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not big.
False
3
inv-proof
[(((((triple12) -> rule6)) -> rule3))]
("Harry" "is" "big" "-")
((((triple12) -> (rule6 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
True
6
proof
[(((((((triple12) -> rule6)) -> rule3) ((triple12) -> rule6)) -> rule4))]
("Harry" "is" "kind" "+")
((((((triple12) -> (rule6 % int3))) -> (rule3 % int2)) ((triple12) -> (rule6 % int3))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not kind.
False
6
inv-proof
[(((((((triple12) -> rule6)) -> rule3) ((triple12) -> rule6)) -> rule4))]
("Harry" "is" "kind" "-")
((((((triple12) -> (rule6 % int3))) -> (rule3 % int2)) ((triple12) -> (rule6 % int3))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is smart.
True
7
proof
[(((((((((triple12) -> rule6)) -> rule3) ((triple12) -> rule6)) -> rule4)) -> rule2))]
("Harry" "is" "smart" "+")
((((((((triple12) -> (rule6 % int4))) -> (rule3 % int3)) ((triple12) -> (rule6 % int4))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Harry is not smart.
False
7
inv-proof
[(((((((((triple12) -> rule6)) -> rule3) ((triple12) -> rule6)) -> rule4)) -> rule2))]
("Harry" "is" "smart" "-")
((((((((triple12) -> (rule6 % int4))) -> (rule3 % int3)) ((triple12) -> (rule6 % int4))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Harry is green.
True
9
proof
[(((((((((((triple12) -> rule6)) -> rule3) ((triple12) -> rule6)) -> rule4)) -> rule2) triple11) -> rule1))]
("Harry" "is" "green" "+")
((((((((((triple12) -> (rule6 % int5))) -> (rule3 % int4)) ((triple12) -> (rule6 % int5))) -> (rule4 % int3))) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
int5
Harry is not green.
False
9
inv-proof
[(((((((((((triple12) -> rule6)) -> rule3) ((triple12) -> rule6)) -> rule4)) -> rule2) triple11) -> rule1))]
("Harry" "is" "green" "-")
((((((((((triple12) -> (rule6 % int5))) -> (rule3 % int4)) ((triple12) -> (rule6 % int5))) -> (rule4 % int3))) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
int5
Fiona is not big.
Unknown
inv-rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Fiona" "is" "big" "-")
Gary is big.
Unknown
rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Gary" "is" "big" "+")
Gary is not kind.
Unknown
inv-rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Gary" "is" "kind" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "red" "+")
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "red" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Dave is big.[(triple1 OR ((triple3) -> rule3))] Dave is green.[(triple2 OR ((triple4 triple5) -> rule1) OR ((((triple1) -> rule5) triple5) -> rule1) OR ((((((triple3) -> rule3)) -> rule5) triple5) -> rule1) OR ((((((triple1 triple3) -> rule4)) -> rule2) triple5) -> rule1) OR ((((((((triple3) -> rule3) triple3) -> rule4)) -> rule2) triple5) -> rule1))] Dave is red.[(triple3)] Dave is smart.[(triple4 OR ((triple1) -> rule5) OR ((((triple3) -> rule3)) -> rule5) OR ((((triple1 triple3) -> rule4)) -> rule2) OR ((((((triple3) -> rule3) triple3) -> rule4)) -> rule2))] Dave is white.[(triple5)] Fiona is green.[(triple6 OR ((((triple7) -> rule2) triple8) -> rule1))] Fiona is kind.[(triple7)] Fiona is white.[(triple8)] Gary is green.[(triple9)] Gary is smart.[(triple10)] Harry is white.[(triple11)] Harry is young.[(triple12)] @1: Dave is kind.[(((triple1 triple3) -> rule4) OR ((((triple3) -> rule3) triple3) -> rule4))] Fiona is smart.[(((triple7) -> rule2))] Harry is red.[(((triple12) -> rule6))] @2: Harry is big.[(((((triple12) -> rule6)) -> rule3))] @3: Harry is kind.[(((((((triple12) -> rule6)) -> rule3) ((triple12) -> rule6)) -> rule4))] @4: Harry is smart.[(((((((((triple12) -> rule6)) -> rule3) ((triple12) -> rule6)) -> rule4)) -> rule2))] @5: Harry is green.[(((((((((((triple12) -> rule6)) -> rule3) ((triple12) -> rule6)) -> rule4)) -> rule2) triple11) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple3) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple2
((triple4 triple5) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple1) -> (rule5 % int2)) triple5) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2)) triple5) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((triple1 triple3) -> (rule4 % int3))) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((((((triple3) -> (rule3 % int4)) triple3) -> (rule4 % int3))) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
((triple1) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple1 triple3) -> (rule4 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((((triple3) -> (rule3 % int3)) triple3) -> (rule4 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
((((triple7) -> (rule2 % int2)) triple8) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple7
Fiona is white.
("Fiona" "is" "white" "+")
triple8
Gary is green.
("Gary" "is" "green" "+")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Harry is white.
("Harry" "is" "white" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Dave is kind.
("Dave" "is" "kind" "+")
((triple1 triple3) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple3) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple12) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((((triple12) -> (rule6 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((((triple12) -> (rule6 % int3))) -> (rule3 % int2)) ((triple12) -> (rule6 % int3))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((((((((triple12) -> (rule6 % int4))) -> (rule3 % int3)) ((triple12) -> (rule6 % int4))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
((((((((((triple12) -> (rule6 % int5))) -> (rule3 % int4)) ((triple12) -> (rule6 % int5))) -> (rule4 % int3))) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
int5