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