Bob is blue. Bob is smart. Charlie is blue. Charlie is smart. Charlie is young. Dave is not big. Dave is furry. Dave is not kind. Fiona is furry. Fiona is rough. If someone is smart then they are big. Big people are kind. Smart people are kind. Big, furry people are young. If someone is big and young then they are furry. If Bob is blue and Bob is not big then Bob is rough. If someone is rough and smart then they are not blue. If Fiona is smart and Fiona is not kind then Fiona is young.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If someone is smart then they are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Smart people are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Big, furry people are young.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If someone is big and young then they are furry.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If Bob is blue and Bob is not big then Bob is rough.
((("Bob" "is" "blue" "+") ("Bob" "is" "big" "~")) -> ("Bob" "is" "rough" "+"))
If someone is rough and smart then they are not blue.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "-"))
If Fiona is smart and Fiona is not kind then Fiona is young.
((("Fiona" "is" "smart" "+") ("Fiona" "is" "kind" "~")) -> ("Fiona" "is" "young" "+"))
Dave is not big.
True
1
proof
[(triple6)]
("Dave" "is" "big" "-")
triple6
Charlie is not blue.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "blue" "-")
triple3
Bob is kind.
True
2
proof
[(((triple2) -> rule3) OR ((((triple2) -> rule1)) -> rule2))]
("Bob" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Charlie is not kind.
False
2
inv-proof
[(((triple4) -> rule3) OR ((((triple4) -> rule1)) -> rule2))]
("Charlie" "is" "kind" "-")
((triple4) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
True
4
proof
[(((((triple4) -> rule1) triple5) -> rule5))]
("Charlie" "is" "furry" "+")
((((triple4) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not furry.
False
4
inv-proof
[(((((triple4) -> rule1) triple5) -> rule5))]
("Charlie" "is" "furry" "-")
((((triple4) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Fiona is not young.
Unknown
inv-rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Fiona" "is" "young" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not young.
Unknown
inv-rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Bob" "is" "young" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Bob is blue.[(triple1)] Bob is smart.[(triple2)] Charlie is blue.[(triple3)] Charlie is smart.[(triple4)] Charlie is young.[(triple5)] Dave is furry.[(triple7)] Dave is not big.[(triple6)] Dave is not kind.[(triple8)] Fiona is furry.[(triple9)] Fiona is rough.[(triple10)] @1: Bob is big.[(((triple2) -> rule1))] Bob is kind.[(((triple2) -> rule3) OR ((((triple2) -> rule1)) -> rule2))] Charlie is big.[(((triple4) -> rule1))] Charlie is kind.[(((triple4) -> rule3) OR ((((triple4) -> rule1)) -> rule2))] @2: Charlie is furry.[(((((triple4) -> rule1) triple5) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple7
Dave is not big.
("Dave" "is" "big" "-")
triple6
Dave is not kind.
("Dave" "is" "kind" "-")
triple8
Fiona is furry.
("Fiona" "is" "furry" "+")
triple9
Fiona is rough.
("Fiona" "is" "rough" "+")
triple10
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((triple4) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple4) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple4) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2