Charlie is blue. Charlie is young. Dave is smart. Fiona is big. Fiona is nice. Gary is big. Gary is blue. All young things are smart. Smart things are big.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
All young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
Smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Dave is smart.
True
1
proof
[(triple3)]
("Dave" "is" "smart" "+")
triple3
Charlie is not young.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "young" "-")
triple2
Dave is big.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "big" "+")
((triple3) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "big" "-")
((triple3) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Charlie is big.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("Charlie" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not big.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("Charlie" "is" "big" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "smart" "-")
Gary is smart.
Unknown
rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "smart" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Charlie is blue.[(triple1)] Charlie is young.[(triple2)] Dave is smart.[(triple3)] Fiona is big.[(triple4)] Fiona is nice.[(triple5)] Gary is big.[(triple6)] Gary is blue.[(triple7)] @1: Charlie is smart.[(((triple2) -> rule1))] Dave is big.[(((triple3) -> rule2))] @2: Charlie is big.[(((((triple2) -> rule1)) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
Fiona is nice.
("Fiona" "is" "nice" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple3) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2