Bob is big. Dave is quiet. Dave is red. Dave is white. Gary is red. Gary is white. Harry is blue. If someone is quiet then they are nice. If someone is blue and big then they are nice. If someone is nice then they are red. All young people are quiet. All big people are young. All young, blue people are white. All nice people are blue.
Bob is big.
("Bob" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If someone is quiet then they are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If someone is blue and big then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
All young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
All big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
All young, blue people are white.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
All nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Gary is red.
True
1
proof
[(triple5)]
("Gary" "is" "red" "+")
triple5
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Bob is young.
True
2
proof
[(((triple1) -> rule5))]
("Bob" "is" "young" "+")
((triple1) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "young" "-")
((triple1) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is blue.
True
3
proof
[(((((triple2) -> rule1)) -> rule7))]
("Dave" "is" "blue" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule7))]
("Dave" "is" "blue" "-")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Bob is nice.
True
4
proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule1))]
("Bob" "is" "nice" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is not nice.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule1))]
("Bob" "is" "nice" "-")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is red.
True
5
proof
[(((((((((triple1) -> rule5)) -> rule4)) -> rule1)) -> rule3))]
("Bob" "is" "red" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is not red.
False
5
inv-proof
[(((((((((triple1) -> rule5)) -> rule4)) -> rule1)) -> rule3))]
("Bob" "is" "red" "-")
((((((((triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is white.
True
8
proof
[(((((triple1) -> rule5) ((((((((triple1) -> rule5)) -> rule4)) -> rule1)) -> rule7)) -> rule6))]
("Bob" "is" "white" "+")
((((triple1) -> (rule5 % int5)) ((((((((triple1) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
int5
Bob is not white.
False
8
inv-proof
[(((((triple1) -> rule5) ((((((((triple1) -> rule5)) -> rule4)) -> rule1)) -> rule7)) -> rule6))]
("Bob" "is" "white" "-")
((((triple1) -> (rule5 % int5)) ((((((((triple1) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
int5
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "young" "-")
Gary is nice.
Unknown
rconc
[@3: Gary is nice.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule5 <- FAIL)]]
("Gary" "is" "nice" "+")
Harry is not red.
Unknown
inv-rconc
[@4: Harry is red.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule4 <- rule5 <- FAIL)]]
("Harry" "is" "red" "-")
Gary is quiet.
Unknown
rconc
[@2: Gary is quiet.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Gary" "is" "quiet" "+")
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "young" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Bob is big.[(triple1)] Dave is quiet.[(triple2)] Dave is red.[(triple3 OR ((((triple2) -> rule1)) -> rule3))] Dave is white.[(triple4)] Gary is red.[(triple5)] Gary is white.[(triple6)] Harry is blue.[(triple7)] @1: Bob is young.[(((triple1) -> rule5))] Dave is nice.[(((triple2) -> rule1))] @2: Bob is quiet.[(((((triple1) -> rule5)) -> rule4))] Dave is blue.[(((((triple2) -> rule1)) -> rule7))] @3: Bob is nice.[(((((((triple1) -> rule5)) -> rule4)) -> rule1))] @4: Bob is blue.[(((((((((triple1) -> rule5)) -> rule4)) -> rule1)) -> rule7))] Bob is red.[(((((((((triple1) -> rule5)) -> rule4)) -> rule1)) -> rule3))] @5: Bob is white.[(((((triple1) -> rule5) ((((((((triple1) -> rule5)) -> rule4)) -> rule1)) -> rule7)) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule5 % int5)) ((((((((triple1) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
int5