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